proposition: Theorem app_flip : forall {X Y} (x : F X) (f : X -> Y), pure f <*> x = pure (flip apply) <*> x <*> pure f.
proof: Proof. intros. rewrite app_interchange. rewrite <- app_composition. rewrite app_fmap_unit. rewrite app_fmap_unit. rewrite app_homomorphism_2. unfold compose. rewrite app_fmap_unit. reflexivity. Qed.
imports: Endo Tuple Coq.Lists.List