proposition: Theorem app_homomorphism_2 : forall {X Y Z} (x : X) (y : Y) (f : X -> Y -> Z), f <$> pure x <*> pure y = pure (f x y).
proof: Proof. intros. rewrite <- app_homomorphism. rewrite <- app_homomorphism. rewrite app_fmap_unit. reflexivity. Qed.
imports: Endo Tuple Coq.Lists.List