The Coq mailing list

[Saint Wesonga <saintwesonga AT gmail.com>]

That proof state was the second portion of "case (V_eq_dec v v0) as [v_eq|v_neq]", so I think there indeed was a contradiction.

On Mon, Apr 23, 2012 at 7:23 AM, Adam Chlipala <adamc AT csail.mit.edu> wrote:

On 04/23/2012 09:20 AM, Bernard Hurley wrote:

I think Saint is trying to obtain a contradiction from the fact that he can prove v = v0 from v = v0 -> False.

There fairly clearly is no contradiction inherent in such a deduction.  For instance, let [v = 0] and [v0 = 0].  The goal would be proved by reflexivity.