Stream: Coq users

Topic: ✔ using False = True hypothesis


view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 22:40):

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

view this post on Zulip Paolo Giarrusso (Jun 06 2022 at 22:41):

Better: exfalso. rewrite H. constructor.

view this post on Zulip Roland Coeurjoly Lechuga (Jun 07 2022 at 19:21):

Both work. Thank you, very ilustrative.

view this post on Zulip Notification Bot (Jun 07 2022 at 19:21):

Roland Coeurjoly has marked this topic as resolved.


Last updated: Jun 24 2024 at 12:02 UTC