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/or3P. - case/hasP => D D1 D2 inS corefS H. apply: corefD1 (corefS). apply: R2 (D1) _ => //. apply: R1 D2 => //. apply: ReqU D1. exact: (SsubU H). - move => H inS corefS ?. apply: corefD1 (corefS). exact: R4 H. - move => H inS corefS ?. apply: corefD1 (corefS). exact: R3 H. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags demo)