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