proposition: Lemma corefD1 S C : ref C -> coref ref S -> coref ref (S `\` [fset C]).
proof: Proof. move => rC coS D. rewrite !in_fsetD negb_and andb_orr -in_fsetD negbK in_fset1. case/orP; first exact: coS. by case/andP => [_ /eqP->]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def)