proposition: Lemma prune_D2_S C s : C \in S -> fAX (fAG s)^- \in C -> demo.fulfillAG (S `|` T) s C.
proof: Proof. move => inS inC. move: (prune_S_aux inS inC). elim. + move => {C inS inC} - C D _ D1 D2 D3. apply: demo.fulfillAG1 D2 D3. by rewrite inE D1. + move => {C inS inC} - C D _ inS0 CD IH1 IH2. apply: demo.fulfillAGn CD _ => //. apply/fsetUP;right. rewrite inE inS0. apply/allP. apply: (@fulfillAG_Req S0 _ s D). exact/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)