proposition: Lemma coref_S : coref ref S.
proof: Proof. Proof using sfc_F. apply: prune_myind => [C|C S]; first by rewrite inE andbN. case/orP. - case/allPn => D. case/fimsetP => t /sepP [inC]. case: (isDiaP t) inC => // s -> inC _ -> /= nS inS corefS subS0. apply: corefD1 (corefS). rewrite (fset1U inC). apply R2 => //. apply: R1 nS => //. move/(subP subS0)/(subP subsep): inS => inU. exact: R1inU. - move => H inS corefS subS0. apply: corefD1 (corefS). case/allPn :H. (do 3 case) => // s [//|] inC. move/(elimN (fulfillAGP _ _ _ _)) => H. case: (boolP (C \in S0)) => [inS0|]. + apply: R3 (inS) inC _ => //. tauto. + by move/(subP subS0) : inS => ->. 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)