rw [append_data' x y]
α : Type u
x y : Array α
⊢ List.length (x ++ y).data = List.length x.data + List.length y.data
α : Type u
x y : Array α
⊢ List.length (x.data ++ y.data) = List.length x.data + List.length y.data