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