rfl
α : Type u
i : Nat
as bs : Array α
h : i ≥ size as
h' : i < size (as ++ bs)
⊢ List.get bs.data { val := i - List.length as.data, isLt := (_ : i - List.length as.data < List.length bs.data) } =
    bs[i - size as]
no goals