proposition: Lemma label_DF (p : DF * DC) (x : Frag p) : leaf x -> label x \in D.
proof: Proof. move/DG7/(_ x) : (FragP p). by case: (leaf _). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)