proposition: Lemma lem_bval_and : forall s e1 e2, bval s (and e1 e2) = bval s e1 && bval s e2.
proof: Proof. induction e1; sauto db: sbool. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String