fact: Definition fulfillAU_step s t (X : {fset clause}) := [fset Y in T | [all C in Req Y, suppS S (t^+ |` C) || [some L in T, suppC L (s^+ |` C) && (L \in X)]]].
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)