∀ (arr : Array Batteries.UFNode) (parentD_lt : ∀ {i : ℕ}, i < arr.size → Batteries.UnionFind.parentD arr i < arr.size)
  (rankD_lt :
    ∀ {i : ℕ},
      Batteries.UnionFind.parentD arr i ≠ i →
        Batteries.UnionFind.rankD arr i < Batteries.UnionFind.rankD arr (Batteries.UnionFind.parentD arr i)),
  sizeOf { arr := arr, parentD_lt := parentD_lt, rankD_lt := rankD_lt } = 1 + sizeOf arr