fact: Definition cnf_of_list {T : Type} (l:list NFormula) (tg : T) : cnf NFormula T := List.fold_right (fun x acc => if check_inconsistent x then acc else ((x,tg)::nil)::acc) (cnf_tt _ _) l.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl