proposition: Lemma eval_map_var `(f: V → W) v s (t: Term V s): eval v (map_var f t) ≡ eval (λ s, v s ∘ f) t.
proof: Proof. induction t; simpl. reflexivity. congruence. reflexivity. Qed.
imports: Coq.Lists.List MathClasses.interfaces.abstract_algebra MathClasses.misc.util MathClasses.theory.jections MathClasses.interfaces.ua_basic