Inductive mipMapListIsSorted : list mipMap -> Prop :=
  | MipsOne   : forall m, mipMapListIsSorted [m]
  | MipsCons  : forall mm0 mm1 mxs,
    mipMapLevel mm1 = S (mipMapLevel mm0) ->
      mipMapListIsSorted (mm0 :: mxs) ->
        mipMapListIsSorted (mm1 :: mm0 :: mxs).
