fact: Definition abs_iff (k: kind) (nf1 ff2 f1 tf2 : TFormula TX AF k) (r: kind) (def : TFormula TX AF r) : TFormula TX AF r := if andb (or_is_X nf1 ff2) (or_is_X f1 tf2) then X r (aformula def) else def.
imports: List Refl Bool Relation_Definitions Setoid