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