proposition: Lemma bind_endo_just {c} (f : c -> Maybe c) (m : Maybe c) (x : c) : m >>= f = Just x <-> exists y, f y = Just x /\ m = Just y.
proof: Proof. induction m; simpl; split; intros. - destruct (f a) eqn:?. inversion H; subst. now eexists; eauto. discriminate. - destruct H, H. inversion H0; subst. now rewrite H. - discriminate. - destruct H, H. discriminate. Qed.
imports: Hask.Control.Monad