fact: Fixpoint check_bbc (a_bv: list bool) (bs: list _lit) := match a_bv, bs with | nil, nil => true | v :: a_bv, b::bs => if Lit.is_pos b then match get_form (Lit.blit b), v with | Ftrue, true | Ffalse, false => check_bbc a_bv bs | _, _ => false end else false | _, _ => false end.
imports: Int63 PArray SMT_classes ZArith Misc State SMT_terms BVList Psatz Bool List BoolEq NZParity Nnat BinPos BinNat Pnat Init.Peano ProofIrrelevance