proposition: Lemma eval_map_var {V W} (f: V → W) v e: eval v (map_var f e) = eval (v ∘ f) e.
proof: Proof. induction e; simpl; try reflexivity. rewrite IHe1, IHe2. reflexivity. Qed.
imports: Coq.Classes.Morphisms Coq.Program.Program Coq.Unicode.Utf8