The Coq mailing list

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

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.