fact: Fixpoint rxcnf {TX : kind -> Type} {AF: Type}(polarity : bool) (k: kind) (f : TFormula TX AF k) : cnf * Trace := match f with | TT _ => if polarity then (cnf_tt, null) else (cnf_ff, null) | FF _ => if polarity then (cnf_ff, null) else (cnf_tt, null) | X b p => if polarity then (cnf_ff, null) else (cnf_ff, null) | A _ x t => ratom (if polarity then normalise x t else negate x t) t | NOT e => rxcnf (negb polarity) e | AND e1 e2 => rxcnf_and rxcnf polarity e1 e2 | OR e1 e2 => rxcnf_or rxcnf polarity e1 e2 | IMPL e1 a e2 => rxcnf_impl rxcnf polarity e1 e2 | IFF e1 e2 => rxcnf_iff rxcnf polarity e1 e2 | EQ e1 e2 => rxcnf_iff rxcnf polarity e1 e2 end.
imports: List Refl Bool Relation_Definitions Setoid