Definition binaryExpArrayMipMap (m : arrayMipMap) : binaryExp := BiRecord [
  ("arrayMipMapLevel",            u32 (arrayMipMapLevel (arrayMipMapIndex m)));
  ("arrayMipMapLayer",            u32 (arrayMipMapLayer (arrayMipMapIndex m)));
  ("arrayMipMapDataOffset",       u64 (arrayMipMapOffset m));
  ("arrayMipMapSizeUncompressed", u64 (arrayMipMapSizeUncompressed m));
  ("arrayMipMapSizeCompressed",   u64 (arrayMipMapSizeCompressed m));
  ("arrayMipMapCRC32",            u32 (arrayMipMapCRC32 m))
].
