rewrite [List.get_append_right' h]
α : Type u
i : Nat
as bs : Array α
h : i ≥ size as
h' : i < size (as ++ bs)
⊢ List.get (as.data ++ bs.data)
      { val := { val := i, isLt := h' }.val,
        isLt := (_ : { val := i, isLt := h' }.val < List.length (as.data ++ bs.data)) } =
    bs[i - size as]
α : 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]