proposition: Lemma alt_endo_just {c} (m n : Maybe c) (x : c) : m <|> n = Just x <-> m = Just x \/ (m = Nothing /\ n = Just x).
proof: Proof. induction m; simpl; intuition auto; discriminate. Qed.
imports: Category.Lib Category.Theory.Functor Category.Theory.Coq.Functor.Proofs Category.Theory.Coq.Applicative.Proofs Category.Theory.Coq.Monad.Proofs Category.Theory.Coq.Maybe