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