Inductive cubeMipMapListIsSorted : list cubeMipMap → Prop :=
  | CubeOne   : ∀ m, cubeMipMapListIsSorted [m]
  | CubeCons  : ∀ mm0 mm1 mxs,
    cubeMapLevel mm1 = S (cubeMapLevel mm0) →
      cubeMipMapListIsSorted (mm0 :: mxs) →
        cubeMipMapListIsSorted (mm1 :: mm0 :: mxs).
