proposition: Theorem ixapp_homomorphism_2 : ∀ {I X Y Z} (x : X) (y : Y) (f : X → Y → Z), f <$$> ixpure x <**> ixpure y = @ixpure _ _ _ I _ (f x y).
proof: Proof. intros. rewrite <- ixapp_homomorphism. rewrite <- ixapp_homomorphism. rewrite app_ixmap_unit. reflexivity. Qed.
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple