Stream: Coq users

Topic: ✔ using False = True hypothesis

Roland Coeurjoly Lechuga (Jun 06 2022 at 22:33):

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

Paolo Giarrusso (Jun 06 2022 at 22:40):

for instance assert False as []. rewrite H. constructor.

Paolo Giarrusso (Jun 06 2022 at 22:41):

Better: exfalso. rewrite H. constructor.

Roland Coeurjoly Lechuga (Jun 07 2022 at 19:21):

Both work. Thank you, very ilustrative.

Notification Bot (Jun 07 2022 at 19:21):

Roland Coeurjoly has marked this topic as resolved.

Last updated: Oct 04 2023 at 23:01 UTC