Definition arrayMipMapsHaveSameLayers : (list arrayMipMap) -> nat -> nat -> Prop :=
  fun m level0 level1 =>
    In level0 (arrayMipMapLevels m) ->
      In level1 (arrayMipMapLevels m) ->
        arrayMipMapLayerCountForLevel level0 m = arrayMipMapLayerCountForLevel level1 m.
