proposition: Lemma dag_D (p : DF * DC) (x : Frag p) s : ~~ leaf x -> fAX s^- \in label x -> exists2 y, edge x y & label y |> s^-.
proof: Proof. move => nl /in_Req H. move/DG3 : (FragP p) => /(_ x nl _ H) [y]. rewrite suppCU suppC1. exists y => //; bcase. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)