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

State before:
α : Type u_1
xs ys : List α
z : α
⊢ xs ++ (ys ++ [z]) = xs ++ ys ++ [z]
Tactic:
apply list_app_assoc
State after:
no goals