fact: Definition unpickle p := match p with | (1,n) => obind (Some \o aAG) (unpickle n) | (2,n) => obind (Some \o aAXG) (unpickle n) | (3,_) => Some aVoid | _ => None end.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.Kstar(Kstar_def)