proposition: Theorem ixapp_embed : ∀ {GI G} `{IxApplicative GI G} {I J K X Y} (x : G I J (X → Y)) (y : G J K X), ixpure (x <**> y) = ixpure ixap <**> ixpure x <**> @ixpure _ _ _ K _ y.
proof: Proof. intros. rewrite_ixapp_homomorphisms. rewrite <- ixapp_homomorphism. rewrite <- app_ixmap_unit. reflexivity. Qed.
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple