The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 05/02/2013 12:00 PM, 
mtkhan AT risc.uni-linz.ac.at
 wrote:
> I have the following inductive definition of stack.
>
> Inductive stack  :=
>    | Create : stack
>    | Push : stack ->  Z ->  stack .
>
> and how can I proceed if I have the following goal.
>
>    r : stack_rep
>    h1 : invariant_stack r
>    h2 : concrete_stack Create r
>    s : stack
>    z : Z
>    ============================
>     Create = Push s z
>
> in fact, this cannot be possible.
>    

When the conclusion formula is false, you need to find a contradiction 
from the hypotheses.  Are you asking how to prove contradictions in general?