fact: Fixpoint check_not (bs br : list _lit) := match bs, br with | nil, nil => true | b::bs, r::br => (r =? Lit.neg b) && check_not bs br | _, _ => 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