proposition: Lemma fulfillAGP s C : reflect (C \in S0 /\ fulfillAG S0 S s C) (C \in fulfillAGb s).
proof: Proof. apply: (iffP idP). - move: C. apply: fset.lfp_ind=> C X IH /sepP [-> /andP[/allP A]]. case/orP => /hasP [D inS] H; split => //. + move: H. rewrite suppCU suppC1 => /andP[H ?]. exact: fulfillAG1 H. + case/andP: H => CD H2. apply: fulfillAGn CD _ => //. by apply IH. - case => inS H. elim: H inS => {C} - C D Req DinS CD. + move => Ds CinS. rewrite fulfillAGE inE CinS andTb. apply/andP;split; first exact/allP. leftb. apply/hasP; exists D => //. by rewrite suppCU suppC1 /= Ds. + move => _ /(_ DinS) HD CinS. rewrite fulfillAGE inE CinS andTb. apply/andP;split; first exact/allP. rightb. apply/hasP; exists D => //. bcase. 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)