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.
discriminate should work
Mathieu Dehouck has marked this topic as resolved.
Last updated: Feb 08 2023 at 22:03 UTC