proposition: Lemma option_equiv_eq {A} (x y : option A) : @option_equiv A (≡) x y ↔ x ≡ y.
proof: Proof. split. induction 1. now f_equal. reflexivity. intros. subst. now assert (@Setoid A (@eq A)) by (split; apply _). Qed.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.monads MathClasses.theory.jections MathClasses.theory.monads