fact: Definition cnf_normalise {T: Type} (t: Formula C) (tg: T) : cnf NFormula T := let f := normalise t in if check_inconsistent f then cnf_ff _ _ else cnf_of_list (xnormalise f) tg.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl