proposition: Lemma subst_eval o V (v: Vars _ ClosedTerm0 _) (t: Term _ V o): @eval _ other _ _ _ (λ x y, eval_in_other (v x y)) t = eval_in_other (close _ v t).
proof: Proof. induction t; simpl. reflexivity. apply IHt1. auto. apply (@algebra_propers et other _ _ _ o). Qed.
imports: Coq.Classes.RelationClasses Coq.Relations.Relation_Definitions Coq.Lists.List Coq.Classes.Morphisms MathClasses.interfaces.universal_algebra MathClasses.theory.ua_homomorphisms MathClasses.interfaces.abstract_algebra MathClasses.interfaces.canonical_names MathClasses.theory.categories MathClasses.categories.varieties