fact: Definition MRel (x y : MType) := lift_edge x y || (let: (existT p a, (existT q a')) := (x,y) in [&& leaf a, q.1 == next p.1, edge (root (Frag q)) a' & label a == val q.2 ]).
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)