∀ {α : Type u_1} (arr : Subarray α) (i : ℕ),
  arr.take i =
    {
      internalRepresentation :=
        { array := arr.array, start := arr.start, stop := min (arr.start + i) arr.stop, start_le_stop := ⋯,
          stop_le_array_size := ⋯ } }