fact: Definition cnf_of_list {T: Type} (tg : T) (l : list (NFormula Z)) := List.fold_right (fun x acc => if Zunsat x then acc else ((x,tg)::nil)::acc) (cnf_tt _ _) l.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums