Theorem: list_app_assoc_reverse (Katydid/Std/Lists.lean)

State before:
α : Type u_1
xs ys zs : List α
⊢ xs ++ ys ++ zs = xs ++ (ys ++ zs)
Tactic:
apply Eq.symm
State after:
case h
α : Type u_1
xs ys zs : List α
⊢ xs ++ (ys ++ zs) = xs ++ ys ++ zs

State before:
case h
α : Type u_1
xs ys zs : List α
⊢ xs ++ (ys ++ zs) = xs ++ ys ++ zs
Tactic:
apply list_app_assoc
State after:
no goals