proposition: Lemma eval_map {V W:Type0 } (f : V -> W) v e : eval v (expr_map f e) = eval (Compose@{Set Set U} v f) e.
proof: Proof. induction e;simpl;try reflexivity;apply ap011;auto. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra