fact: Definition pickle A := match A with | aAU s => (1,pickle s) | aAXU s => (2,pickle s) | aVoid => (3,0) | aAR s => (4,pickle s) | aAXR s => (5,pickle s) end.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base) CompDecModal.CTL(CTL_def)