2

How can I prove 

Goal False = (0<>0).

?

I tried omega, and I could not find any lemma that contains (False = ) or ( = False).

Necto
  • 2,594
  • 1
  • 20
  • 45
  • The issue requires the exact same answer you made, but I would not flag it as dup – Vinz Sep 15 '15 at 14:22
  • 1
    Note that the proof of the bi-implication `False <-> (0<>0)` is easy to prove with `omega`. – Konstantin Weitz Sep 16 '15 at 14:42
  • Yep, thanks. I used to think that `<->` and `=` are interchangeable for `Prop` but apparently they are not, at least in 8.4 – Necto Sep 17 '15 at 12:17
  • as Arthur explains in the other question, it never has been the case "in general". @KonstantinWeitz `intuition` is enough, no need to invoke the all-mighty omega here :D – Vinz Sep 18 '15 at 07:21

0 Answers0