Inductive arrayMipMapList : Set := ArrayMipMapList {
  arrayMipMaps                : list arrayMipMap;
  arrayMipMapIndicesAreSorted : arrayMipMapIndicesSorted (map arrayMipMapIndex arrayMipMaps);
  arrayMipMapOffsetAreSorted  : arrayMipMapOffsetsSorted arrayMipMaps;
  arrayMipMapSameLayers       : forall level0 level1, arrayMipMapsHaveSameLayers arrayMipMaps level0 level1
}.
