Definition binaryExpCompression (c : compressionMethod) : binaryExp := BiRecord [
  ("descriptor",        utf8 (descriptorOf c));
  ("sectionIdentifier", u64 (compressionSectionIdentifier c));
  ("blockSizeX",        u32 (compressionBlockSizeX c));
  ("blockSizeY",        u32 (compressionBlockSizeY c));
  ("blockAlignment",    u32 (compressionBlockAlignment c))
].
