proposition: Lemma is_Some_def `(x : option A) : is_Some x ↔ ∃ y, x ≡ Some y.
proof: Proof. unfold is_Some. destruct x; firstorder (eauto; discriminate). Qed.
imports: Coq.Program.Program Coq.Classes.Morphisms Coq.Setoids.Setoid MathClasses.interfaces.canonical_names