fact: Definition lt_form i h := match h with | Fatom _ | Ftrue | Ffalse => true | Fnot2 _ l => Lit.blit l <? i | Fand args | For args | Fimp args => aforallbi (fun _ l => Lit.blit l <? i) args | Fxor a b | Fiff a b => (Lit.blit a <? i) && (Lit.blit b <? i) | Fite a b c => (Lit.blit a <? i) && (Lit.blit b <? i) && (Lit.blit c <? i) | FbbT _ ls => List.forallb (fun l => Lit.blit l <? i) ls end.
imports: Bool Int63 Psatz PArray BinNat BinPos ZArith SMT_classes_instances Misc State BVList