proposition: Lemma Maybe_choose_spec {a} {x y : Maybe a} : isJust (x <|> y) = (isJust x || isJust y)%bool.
proof: Proof. destruct x; auto. 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