fact: Fixpoint beval (st : state) (b : bexp) : bool := match b with | BTrue => true | BFalse => false | BEq a1 a2 => Nat.eqb (aeval st a1) (aeval st a2) | BLe a1 a2 => leb (aeval st a1) (aeval st a2) | BNot b1 => negb (beval st b1) | BAnd b1 b2 => andb (beval st b1) (beval st b2) end.
imports: Mtac2(Datatypes List Mtac2 ConstrSelector) Coq.Arith.Arith Coq.Arith.EqNat