fact: Fixpoint map_bformula (k: kind)(fct : TA -> TA') (f : @GFormula TA TX AA AF k) : @GFormula TA' TX AA AF k:= match f with | TT k => TT k | FF k => FF k | X k p => X k p | A k a t => A k (fct a) t | AND f1 f2 => AND (map_bformula fct f1) (map_bformula fct f2) | OR f1 f2 => OR (map_bformula fct f1) (map_bformula fct f2) | NOT f => NOT (map_bformula fct f) | IMPL f1 a f2 => IMPL (map_bformula fct f1) a (map_bformula fct f2) | IFF f1 f2 => IFF (map_bformula fct f1) (map_bformula fct f2) | EQ f1 f2 => EQ (map_bformula fct f1) (map_bformula fct f2) end.
imports: List Refl Bool Relation_Definitions Setoid