rewrite [getElem_eq_data_get]
α : Type u
i : Nat
as bs : Array α
h : i < size as
h' : i < size (as ++ bs)
⊢ (as ++ bs)[i] = as[i]
α : Type u
i : Nat
as bs : Array α
h : i < size as
h' : i < size (as ++ bs)
⊢ List.get (as ++ bs).data { val := i, isLt := h' } = as[i]