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:
But nothing works
assert False as . rewrite H. constructor.
exfalso. rewrite H. constructor.
Both work. Thank you, very ilustrative.
Roland Coeurjoly has marked this topic as resolved.
Last updated: Oct 04 2023 at 23:01 UTC