proposition: Lemma coref_DD : coref pref DD.
proof: Proof. apply: prune_myind => [C|C S]; first by rewrite inE andbN. case/allPn. case. case => // p s. case => // inC H inS corS sub. apply: corefD1 => //. exact: (P2 sub). Qed.
imports: Relations Classical_Pred_Type mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base) CompDecModal.PDL(PDL_def)