fact: Definition check_normalised_formulas : list NFormula -> Psatz -> bool := fun l cm => match eval_Psatz l cm with | None => false | Some f => check_inconsistent f end.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl