proposition: Lemma prune_D2 : D2 (S `|` T).
proof: Proof. move => C. case/fsetUP; first by move => *; exact: prune_D2_S. move => inT s inC. have inST : C \in S `|` T by rewrite inE inT. case/hasP : (prune_D1_strong inC inST) => D. rewrite suppCU suppC1 => D1 /andP [/= D2 D3]. case/orP : D2 => Hs. - apply: demo.fulfillAG1 D3 _ => //. by rewrite inE D1. - apply: demo.fulfillAGn D3 _; first by rewrite inE D1. exact: prune_D2_S. 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)