fact: Fixpoint xcnf {TX : kind -> Type} {AF: Type} (pol : bool) (k: kind) (f : TFormula TX AF k) {struct f}: cnf := match f with | TT _ => if pol then cnf_tt else cnf_ff | FF _ => if pol then cnf_ff else cnf_tt | X _ p => if pol then cnf_ff else cnf_ff | A _ x t => if pol then normalise x t else negate x t | NOT e => xcnf (negb pol) e | AND e1 e2 => mk_and xcnf pol e1 e2 | OR e1 e2 => mk_or xcnf pol e1 e2 | IMPL e1 _ e2 => mk_impl xcnf pol e1 e2 | IFF e1 e2 => match is_bool e2 with | Some isb => xcnf (if isb then pol else negb pol) e1 | None => mk_iff xcnf pol e1 e2 end | EQ e1 e2 => match is_bool e2 with | Some isb => xcnf (if isb then pol else negb pol) e1 | None => mk_iff xcnf pol e1 e2 end end.
imports: List Refl Bool Relation_Definitions Setoid