proposition: Lemma lem_equal : forall s e1 e2, eval s (simp_equal 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