forall (f : TermAlgebra C $-> A), hom_term_algebra A (precomp_var_term_algebra f) = f. Proof. intro f. apply path_homomorphism. funext s T. induction T as [|u c h]. - reflexivity. - refine (_ @ (is_homomorphism f u c)^). refine (ap u.#A _). funext i. apply h. Defined.
Require Import