proposition: Lemma root_internal (p : DF * DC) : ~~ leaf (root (Frag p)).
proof: Proof. by move/DG6 : (FragP p). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)