Definition arrayMipMapFirst (m : arrayMipMapList) : arrayMipMap.
