Stream: Coq users

Topic: Hypothesis statement


view this post on Zulip pianke (Jan 20 2022 at 15:17):

I have hypothesis
H: true = true \/ true = false
With the help of above H , a goal can be close (by inversion-right side of H) ?

view this post on Zulip Théo Winterhalter (Jan 20 2022 at 15:18):

H will not help you to do much, since it's a tautology.

view this post on Zulip Michael Soegtrop (Jan 20 2022 at 16:50):

I guess you mixed up /\ and \/ here. With /\, the hypothesis would be equivalent to False. With \/ it is equivalent to True.


Last updated: Jan 28 2023 at 06:30 UTC