proposition: Lemma ref_coref S C : C \in U -> coref F gen S -> (forall D, D \in base S C -> gen D) -> gen C.
proof: Proof. Proof using sfc_F. move => inU corefS baseP. apply: ref_R0 inU _ => D /sepP [D1 D2]. case: (boolP (D \in S)) => H; first by apply: baseP; rewrite inE H. apply: corefS. by rewrite inE D1. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.K(K_def demo)