fact: Fixpoint aformula (k: kind) (f : TFormula TX AF k) : TX k := match f with | TT b => mkTT b | FF b => mkFF b | X b p => p | A b x t => mkA b x t | AND f1 f2 => mkAND (aformula f1) (aformula f2) | OR f1 f2 => mkOR (aformula f1) (aformula f2) | IMPL f1 o f2 => mkIMPL (aformula f1) (aformula f2) | IFF f1 f2 => mkIFF (aformula f1) (aformula f2) | NOT f => mkNOT (aformula f) | EQ f1 f2 => mkEQ (aformula f1) (aformula f2) end.
imports: List Refl Bool Relation_Definitions Setoid