Definition binaryExpCubeMipMapFace (m : cubeMapFace) : binaryExp := BiRecord [
  ("cubeFaceDataOffset",       u64 (cubeFaceOffset m));
  ("cubeFaceSizeUncompressed", u64 (cubeFaceSizeUncompressed m));
  ("cubeFaceSizeCompressed",   u64 (cubeFaceSizeCompressed m));
  ("cubeFaceCRC32",            u32 (cubeFaceCRC32 m))
].
