simplifies subterms like 5 + 7 to 12. Using the auxiliary function simp_const, define a function “fuse”: to simplify a plus or a times, first simplify the arguments recursively, and then apply simp_const := e def fuse : aexpr → aexpr := sorry theorem simp_const_eq (v : N → N) : ∀ e : aexpr, aeval v (simp_const e) = aeval v e := sorry theorem fuse_eq (v : N → N) : ∀ e : aexpr, aeval v (fuse e) = aeval