proposition: Lemma leaf_root' s t (p : DF * DC) (x : Frag p) (lf : leaf x) : EU_M s t (Mstate (root (Frag (next p.1, SeqSub _ (label_DF lf))))) -> EU_M s t (Mstate x).
proof: Proof. move => R. apply: cEU_eq R; try by rewrite /= label_root. exact: leaf_root_aux. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)