proposition: Lemma coref_DD : coref ref DD.
proof: Proof. Proof using sfc_F. apply: prune_myind => [C|C S]; first by rewrite inE andbN. case/orP. - case/allPn. (do 2 case) => // 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 ?. apply: corefD1 (corefS). case/allPn :H. (do 3 case) => // s [//|] inC. move/(elimN (fulfillAGP _ _ _)) => H. apply: R3 (inS) inC _ => //. tauto. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.Kstar(Kstar_def)