proposition: Lemma lem_simp {A} : forall s (e : expr A), eval s (simp e) = eval s e.
proof: Proof. time (depind e; sauto use: lem_plus, lem_equal, @lem_fst, @lem_snd, @lem_ite). Undo. time (depind e; sauto db: simp_db). Undo. time (depind e; simpl; autorewrite with simp_db; sauto). Qed.
imports: Hammer(Tactics) Program.Equality Arith String