proposition: Theorem iapp_embed : forall {G : Type -> Type -> Type -> Type} `{IApplicative G} {I J K X Y} (x : G I J (X -> Y)) (y : G J K X), ipure (x <**> y) = ipure iap <**> ipure x <**> @ipure _ _ K _ y.
proof: Proof. intros. rewrite_iapp_homomorphisms. rewrite <- iapp_homomorphism. rewrite <- app_imap_unit. reflexivity. Qed.
imports: Hask.Ltac Hask.Prelude FunctionalExtensionality