fact: Definition pickle A := match A with | aAG s => (1,pickle s) | aAXG s => (2,pickle s) | aVoid => (3,0) end.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.Kstar(Kstar_def)