proposition: Lemma fulfillAG_Req S0 S s C : C \in fulfillAGb S0 S s -> (forall E, E \in Req C -> suppS S E).
proof: Proof. by case/fulfillAGP => _ []. Qed.
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)