Definition binaryExpCubeMipMap (m : cubeMipMap) : binaryExp := BiRecord [
  ("cubeMipMapLevel",    u32 (cubeMapLevel m));
  ("cubeMipMapFacePosX", binaryExpCubeMipMapFace (cubeMapFaceXPos m));
  ("cubeMipMapFaceNegX", binaryExpCubeMipMapFace (cubeMapFaceXNeg m));
  ("cubeMipMapFacePosY", binaryExpCubeMipMapFace (cubeMapFaceYPos m));
  ("cubeMipMapFaceNegY", binaryExpCubeMipMapFace (cubeMapFaceYNeg m));
  ("cubeMipMapFacePosZ", binaryExpCubeMipMapFace (cubeMapFaceZPos m));
  ("cubeMipMapFaceNegZ", binaryExpCubeMipMapFace (cubeMapFaceZNeg m))
].
