proposition: Theorem iapp_flip : forall {J K X Y} (x : F J K X) (f : X -> Y), ipure f <**> x = ipure (flip apply) <**> x <**> ipure f.
proof: Proof. intros. rewrite iapp_interchange. rewrite <- iapp_composition. rewrite app_imap_unit. rewrite app_imap_unit. rewrite iapp_homomorphism_2. unfold comp. rewrite app_imap_unit. reflexivity. Qed.
imports: Hask.Ltac Hask.Prelude FunctionalExtensionality