proposition: Lemma lem_simp {A} : forall s (e : expr A), eval s (simp e) = eval s e.
proof: Proof. depind e; sauto db: simp_db. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String Relations Sorting.Permutation Program.Equality