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