proposition: Lemma lem_equal : forall s e1 e2, eval s (simp_equal e1 e2) = (eval s e1 =? eval s e2).
proof: Proof. Fail depind e1; sauto. time (depind e1; sauto dep: on). Undo. time (depind e1; depelim e2; sauto). Qed.
imports: Hammer(Tactics) Program.Equality Arith String