proposition: Lemma lem_bval_bsimp : forall s e, bval s (bsimp e) = bval s e.
proof: Proof. induction e; sauto use: lem_bval_not, lem_bval_and, lem_bval_less. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String