fact: Fixpoint bval (s : state) (e : bexpr) := match e with | Bval b => b | Bnot e1 => negb (bval s e1) | Band e1 e2 => bval s e1 && bval s e2 | Bless a1 a2 => aval s a1 <? aval s a2 end.
imports: Hammer(Tactics Reflect) String Arith Lia