proposition: Lemma sn_edge (p : DF * DC) (x : Frag p) : sn (edge (g := Frag p)) x.
proof: Proof. by move/DG2 : (FragP p). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)