fact: Definition xnegate (t:NFormula) : list (NFormula) := let (e,o) := t in match o with | Equal => (e,Equal) :: nil | NonEqual => (e,Strict)::(popp e,Strict)::nil | Strict => (e,Strict) :: nil | NonStrict => (e,NonStrict) :: nil end.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl