fact: Definition abs_not (k: kind) (f1 : TFormula TX AF k) (c : forall (k: kind), TFormula TX AF k -> TFormula TX AF k) := match is_X f1 with | Some _ => X k (aformula (c k f1 )) | _ => c k f1 end.
imports: List Refl Bool Relation_Definitions Setoid