Theorem: List1.append_compat_left (GMLInit/Data/List/List1.lean)

State before:
α : Type u_1
β : Type ?u.22157
xs✝ ys : List1 α
zs : List α
x : α
xs : List α
⊢ xs ++ ys.toList ++ zs = xs ++ (ys.append zs).toList
Tactic:
rw [append_toList_left, List.append_assoc]
State after:
no goals