fact: Fixpoint beval (b : bexp) : bool := match b with | BTrue => true | BFalse => false | BEq a1 a2 => beq_nat (aeval a1) (aeval a2) | BLe a1 a2 => leb (aeval a1) (aeval a2) | BNot b1 => negb (beval b1) | BAnd b1 b2 => andb (beval b1) (beval b2) end.
imports: Coq.Bool.Bool Coq.Arith.Arith Coq.Arith.EqNat Coq.omega.Omega Coq.Lists.List Coq.omega.Omega Maps