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