proposition: Lemma fulfillAGP s S C : reflect (C \in S /\ fulfillAG S s C) (C \in fulfillAGb s S).
proof: Proof. apply: (iffP idP). - move: C. apply: fset.lfp_ind => C X IH /sepP[-> /hasP[D inS] /andP[CD]]. case/orP => H; split => //; first exact: fulfillAG1 H. apply: fulfillAGn CD _ => //. by apply IH. - case => inS H. elim: H inS => {C} - C D DinS CD. + move => Ds CinS. rewrite fulfillAGE inE CinS andTb. by apply/hasP; exists D; bcase. + move => _ /(_ DinS) HD CinS. rewrite fulfillAGE inE CinS andTb. by apply/hasP; exists D; bcase. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.Kstar(Kstar_def)