∀ (motive : (x : ByteArray) → (x_1 : ℕ) → UInt8 → x_1 < x.size → Sort u_1) (bs : Array UInt8) (i : ℕ) (b : UInt8)
  (h : i < { data := bs }.size)
  (h_1 : (bs : Array UInt8) → (i : ℕ) → (b : UInt8) → (h : i < { data := bs }.size) → motive { data := bs } i b h),
  (match { data := bs }, i, b, h with
    | { data := bs }, i, b, h => h_1 bs i b h) =
    h_1 bs i b h