fact: Record fragment G u L := { DG1 : label (root G) = L; DG2 : terminates (erel G); DG3 : req_cond G; DG4 : supp_cond G; DG5 : ev_cond u G; DG6 : ~~ leaf (root G); DG7 : glabels_from G }.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)