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.

`discriminate`

should work

perfectly so.

Thank you

Mathieu Dehouck has marked this topic as resolved.

Last updated: Oct 01 2023 at 18:01 UTC