fact: Definition bounded_demo (D Dl : {fset clause}) (n : nat) := forall L u (inFs : u \in Fs D) (inD : L \in D), {G : rGraph clause | fragment D Dl G u L & #|G| <= n}.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)