proposition: Lemma coref_supp C : C \in U -> ~~ suppS S C -> href C.
proof: Proof. Proof using coref_S sfc_F. move => inU sD. rewrite /href. rewrite -> baseP => //. apply: bigOE => D. case/sepP => D1 D2. apply: contraN sD. by apply/hasP; exists D. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.CTL(CTL_def dags demo hilbert relaxed_pruning)