The Coq mailing list

[mtkhan AT risc.uni-linz.ac.at]

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.

Any help or hint here.

regards,
tk