proposition: Theorem app_fmap_compose : forall A B (f : A -> B), pure ∘ f = fmap f ∘ pure.
proof: Proof. intros. extensionality x. unfold compose. rewrite <- app_homomorphism. rewrite app_fmap_unit. reflexivity. Qed.
imports: Endo Tuple Coq.Lists.List