fact: Definition unpickle p := match p with | (1,n) => obind (Some \o aAU) (unpickle n) | (2,n) => obind (Some \o aAXU) (unpickle n) | (3,_) => Some aVoid | (4,n) => obind (Some \o aAR) (unpickle n) | (5,n) => obind (Some \o aAXR) (unpickle n) | _ => None end.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base) CompDecModal.CTL(CTL_def)