proposition: Theorem app_embed : forall {G : Type -> Type} `{Applicative G} {X Y} (x : G (X -> Y)) (y : G X), pure (x <*> y) = pure ap <*> pure x <*> pure y.
proof: Proof. intros. rewrite_app_homomorphisms. rewrite <- app_homomorphism. rewrite <- app_fmap_unit. reflexivity. Qed.
imports: Endo Tuple Coq.Lists.List