proposition: Theorem ixapp_flip : ∀ {J K X Y} (x : F J K X) (f : X → Y), ixpure f <**> x = ixpure (fun a b => b a) <**> x <**> ixpure f.
proof: Proof. intros. rewrite ixapp_interchange. rewrite <- ixapp_composition. rewrite app_ixmap_unit. rewrite app_ixmap_unit. rewrite ixapp_homomorphism_2. unfold comp. rewrite app_ixmap_unit. reflexivity. Qed.
imports: Hask.Ltac Coq.Program.Equality Coq.Unicode.Utf8 FunctionalExtensionality Iso Tuple