The Coq mailing list

[wesongathedeveloper AT yahoo.com]

Hello,

I have a question about the following proof state:


v_neq : v = v0 -> False
______________________________________(1/51)
v = v0

V is an inductive type. I had the hypothesis "v_neq" as v <> v0 since I did
"case (V_eq_dec v v0) as [v_eq|v_neq]." For this branch where v <> v0, I
thought that I would be able to use inversion on v_neq to dispatch this goal.
However, I get the message that the type of v_neq is not inductive. How do I
use this proposition to show that this goal is a contradiction (if this is
possible, I'm still figuring out how Prop is different from the traditional
"boolean" world)?

Thank you,

Saint.