fact: Definition AU_label (x : AU_T0) := match x with inl x => val x | inr x => val x end.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags)