Inductive arrayMipMapIndicesSorted : list arrayMipMapIndexT → Prop :=
  | AMMIOne  : ∀ m, arrayMipMapIndicesSorted [m]
  | AMMICons : ∀ mmx mmy mxs,
    arrayMipMapIndexOrd mmx mmy →
      arrayMipMapIndicesSorted (mmy :: mxs) →
        arrayMipMapIndicesSorted (mmx :: mmy :: mxs).
