proposition: Lemma heq_eval_const vars {o} (t: T et (ne_list.one o)): ` (eval et vars t) = eval et (Pvars vars) t.
proof: Proof. apply (heq_eval vars t). Qed.
imports: Coq.Classes.RelationClasses Coq.Classes.Morphisms Coq.Program.Program MathClasses.interfaces.abstract_algebra MathClasses.interfaces.universal_algebra MathClasses.interfaces.canonical_names MathClasses.theory.ua_subalgebra