proposition: Lemma lem_plus : forall s e1 e2, eval s (simp_plus e1 e2) = eval s e1 + eval s e2.
proof: Proof. depind e1; sauto dep: on. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String Relations Sorting.Permutation Program.Equality