proposition: Theorem app_split : forall A B C (f : A -> B -> C) (x : F A) (y : F B), f <$> x <*> y = uncurry f <$> (x ** y).
proof: Proof. intros. unfold app_prod. repeat (rewrite <- app_fmap_unit). repeat (rewrite <- app_composition; f_equal). repeat (rewrite app_homomorphism). unfold uncurry, compose. f_equal. Qed.
imports: Endo Tuple Coq.Lists.List