proposition: Lemma prune_D1_strong C s : fAX s^- \in C -> C \in S `|` T -> suppS S (s^- |` R C).
proof: Proof. move => inC. have Req_s : (s^- |` R C) \in Req C. apply/fimsetP; exists (fAX s^-) => //. by rewrite inE inC. case/fsetUP. - move/pruneE. rewrite negb_or => /andP [/negPn /allP P _]. exact: P. - by case/sepP => _ /allP /(_ _ Req_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)