Inductive arrayMipMapIndexOrd : arrayMipMapIndexT → arrayMipMapIndexT → Prop :=
  | AMMIOrdEq : ∀ i0 i1,
    i0 = i1 → arrayMipMapIndexOrd i0 i1
  | AMMIOrdLevelEq : ∀ i0 i1,
    arrayMipMapLevel i0 = arrayMipMapLevel i1 →
      arrayMipMapLayer i0 < arrayMipMapLayer i1 →
        arrayMipMapIndexOrd i0 i1
  | AMIIOrdLevelLt : ∀ i0 i1,
    arrayMipMapLevel i1 < arrayMipMapLevel i0 →
      arrayMipMapIndexOrd i0 i1.
