proposition: Lemma option_equiv_alt x y : x = y ↔ (∀ n, x = Some n ↔ y = Some n).
proof: Proof. split; intros E1. intro. now rewrite E1. destruct x, y. now apply E1. symmetry. now apply E1. now apply E1. easy. Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.jections MathClasses.theory.monads