proposition: Lemma prune_S_aux C s : C \in S -> fAX (fAG s)^- \in C -> fulfillAG S0 S s C.
proof: Proof. move => inS inC. move/pruneE : inS. rewrite negb_or => /andP [_ P]. rewrite negbK in P. move/allP : P => /(_ _ inC) /fulfillAGP. tauto. 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)