proposition: Theorem iapp_homomorphism_2 : forall {I X Y Z} (x : X) (y : Y) (f : X -> Y -> Z), f <$$> ipure x <**> ipure y = @ipure _ _ I _ (f x y).
proof: Proof. intros. rewrite <- iapp_homomorphism. rewrite <- iapp_homomorphism. rewrite app_imap_unit. reflexivity. Qed.
imports: Hask.Ltac Hask.Prelude FunctionalExtensionality