Inductive cubeOffsetsSorted : list cubeMipMap → Prop :=
  | CMMSizeOne  : ∀ m,
    cubeFaceExtent (cubeMapFaceXPos m) < cubeFaceOffset (cubeMapFaceXNeg m) →
    cubeFaceExtent (cubeMapFaceXNeg m) < cubeFaceOffset (cubeMapFaceYPos m) →
    cubeFaceExtent (cubeMapFaceYPos m) < cubeFaceOffset (cubeMapFaceYNeg m) →
    cubeFaceExtent (cubeMapFaceYNeg m) < cubeFaceOffset (cubeMapFaceZPos m) →
    cubeFaceExtent (cubeMapFaceZPos m) < cubeFaceOffset (cubeMapFaceZNeg m) →
      cubeOffsetsSorted [m]
  | CMMSizeCons : ∀ mm0 mm1 mxs,
    cubeFaceExtent (cubeMapFaceZNeg mm1) < cubeFaceOffset (cubeMapFaceXPos mm0) →
      cubeOffsetsSorted (mm0 :: mxs) →
        cubeOffsetsSorted (mm1 :: mm0 :: mxs).
