proposition: Theorem iapp_naturality : forall {I J K A B C D} (f : A -> C) (g : B -> D) (u : F I J A) (v : F J K B), imap (f *** g) (u ** v) = (imap f u) ** (imap g v).
proof: Proof. intros. unfold iapp_prod. rewrite <- app_imap_unit. rewrite ifun_composition_x. repeat (rewrite <- app_imap_unit). rewrite <- iapp_composition. rewrite <- iapp_composition. rewrite <- iapp_composition. rewrite <- iapp_composition. rewrite iapp_composition. rewrite iapp_composition. rewrite_iapp_homomorphisms. rewrite ifun_composition_x. rewrite ifun_composition_x. rewrite iapp_interchange. rewrite app_imap_unit. rewrite ifun_composition_x. unfold comp. reflexivity. Qed.
imports: Hask.Ltac Hask.Prelude FunctionalExtensionality