proposition: Lemma DD_refute C : C \in PU -> ~~ DD |> C -> pref C.
proof: Proof. move => inU. apply: P1 _ inU => //. exact: coref_DD. Qed.
imports: Relations Classical_Pred_Type mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base) CompDecModal.PDL(PDL_def)