proposition: Theorem app_naturality : forall {A B C D} (f : A -> C) (g : B -> D) (u : F A) (v : F B), fmap (f *** g) (u ** v) = (fmap f u) ** (fmap g v).
proof: Proof. intros. unfold app_prod. rewrite <- app_fmap_unit. rewrite fun_composition_x. repeat (rewrite <- app_fmap_unit). rewrite <- app_composition. rewrite <- app_composition. rewrite <- app_composition. rewrite <- app_composition. rewrite app_composition. rewrite app_composition. f_equal. rewrite_app_homomorphisms. rewrite fun_composition_x. rewrite fun_composition_x. rewrite app_interchange. rewrite app_fmap_unit. rewrite fun_composition_x. f_equal. Qed.
imports: Endo Tuple Coq.Lists.List