After the inversion of some hypothesis, I have False = True (type Prop, not bool) in the context.
How can you prove the goal with that hypothesis?
I have tried:
discriminate.
exfalso; discriminate.
congruence.
But nothing works
for instance assert False as []. rewrite H. constructor.
Better: exfalso. rewrite H. constructor.
Both work. Thank you, very ilustrative.
Roland Coeurjoly has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC