proposition: Lemma lem_aval_asimp : forall s e, aval s (asimp e) = aval s e.
proof: Proof. induction e; sauto use: lem_aval_plus. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String