proposition: Lemma DD_refute C : C \in U -> ~~ suppS DD C -> ref C.
proof: Proof. Proof using sfc_F. move => inU. apply: R1 inU _ => //. exact: coref_DD. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def)