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/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. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def)