proposition: Lemma bind_endo_nothing {c} (f : c → Maybe c) (m : Maybe c) : m >>= f = Nothing <-> m = Nothing \/ exists y, f y = Nothing /\ m = Just y.
proof: Proof. induction m; simpl; split; intros. - destruct (f a) eqn:?. + unfold bind in H; simpl in H. congruence. + right. now eexists; eauto. - destruct H. + discriminate. + firstorder eauto. inversion_clear H0. now unfold bind; simpl. - now left. - reflexivity. 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