Inductive arrayMipMapIndexOrd : arrayMipMapIndexT -> arrayMipMapIndexT -> Prop :=
  | AMMIOrdEq : forall i0 i1,
    i0 = i1 -> arrayMipMapIndexOrd i0 i1
  | AMMIOrdLevelEq : forall i0 i1,
    arrayMipMapLevel i0 = arrayMipMapLevel i1 ->
      arrayMipMapLayer i0 < arrayMipMapLayer i1 ->
        arrayMipMapIndexOrd i0 i1
  | AMIIOrdLevelLt : forall i0 i1,
    arrayMipMapLevel i1 < arrayMipMapLevel i0 ->
      arrayMipMapIndexOrd i0 i1.
