Mathieu Dehouck (Jan 25 2022 at 13:49): Mathieu Dehouck (Jan 25 2022 at 13:49):Dear All,
I am renew to Coq, and after a lot of struggle, I start to get my way through.
I have a new silly problem : a proof where the goal is "None <> Some a".
Is there a tactic or a lemma somewhere I could use to solve it?
I've looked around, and tried trivial, simpl, auto... I can't seem to find the point.
Best.
Gaëtan Gilbert (Jan 25 2022 at 13:51):discriminate should work
Mathieu Dehouck (Jan 25 2022 at 14:01):perfectly so.
Thank you
Notification Bot (Jan 25 2022 at 14:01):Mathieu Dehouck has marked this topic as resolved.
Last updated: Oct 01 2023 at 18:01 UTC