∀ (array : ByteArray) (start stop : ℕ) (start_le_stop : start ≤ stop) (stop_le_array_size : stop ≤ array.size),
  sizeOf
      { array := array, start := start, stop := stop, start_le_stop := start_le_stop,
        stop_le_array_size := stop_le_array_size } =
    1 + sizeOf array + sizeOf start + sizeOf stop + sizeOf start_le_stop + sizeOf stop_le_array_size