Definition arrayMipMapsHaveSameLayers : (list arrayMipMap) → nat → nat → Prop :=
  λ m level0 level1,
    In level0 (arrayMipMapLevels m) →
      In level1 (arrayMipMapLevels m) →
        arrayMipMapLayerCountForLevel level0 m = arrayMipMapLayerCountForLevel level1 m.
