fact: Fixpoint abst_form (pol : bool) (k: kind) (f : TFormula TX AF k) : TFormula TX AF k:= match f with | TT k => if pol then TT k else X k (mkTT k) | FF k => if pol then X k (mkFF k) else FF k | X k p => X k p | A k x t => if needA t then A k x t else X k (mkA k x t) | AND f1 f2 => abst_and abst_form pol f1 f2 | OR f1 f2 => abst_or abst_form pol f1 f2 | IMPL f1 o f2 => abst_impl abst_form pol o f1 f2 | NOT f => abs_not (abst_form (negb pol) f) NOT | IFF f1 f2 => abst_iff abst_form pol f1 f2 | EQ f1 f2 => abst_eq abst_form pol f1 f2 end.
imports: List Refl Bool Relation_Definitions Setoid