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