proposition: Lemma dag_R (p : DF * DC) (x y : Frag p) : edge x y -> suppC (label y) (R (label x)).
proof: Proof. by move/DG4: (FragP p) => /(_ x y). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)