proposition: Theorem ixapp_split : ∀ I J K A B C (f : A → B → C) (x : F I J A) (y : F J K B), f <$$> x <**> y = uncurry f <$$> (x ** y).
proof: Proof. intros. unfold ixapp_prod. repeat (rewrite <- app_ixmap_unit). repeat (rewrite <- ixapp_composition). repeat (rewrite ixapp_homomorphism). unfold uncurry, comp. reflexivity. Qed.
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple