proposition: Lemma is_None_def `(x : option A) : is_None x ↔ x ≡ None.
proof: Proof. unfold is_None. destruct x; firstorder discriminate. Qed.
imports: Coq.Program.Program Coq.Classes.Morphisms Coq.Setoids.Setoid MathClasses.interfaces.canonical_names