fact: Definition fulfillAGb s S := fset.lfp S (fulfillAG_fun s S).
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.Kstar(Kstar_def)