fact: Definition fulfillAG_fun s X : {fset clause} := [fset C in S0 | [all D in Req C, suppS S D] && (suppS S (s^- |` R C) || [some D in S0, rtrans C D && (D \in X)])].
imports: Relations Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.Kstar(Kstar_def demo hilbert_ref gen_def)