fact: Definition AXn_complete (S : {fset clause}) := forall L C, L \in S -> C \in Req L -> exists L', (L' \in S) && suppC L' C.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)