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

State before:
α : Type u_1
xs : List α
⊢ xs = xs ++ []
Tactic:
cases xs with
| nil => rfl
| cons head tail => simp only [append_nil]
State after:
no goals

State before:
case nil
α : Type u_1
⊢ [] = [] ++ []
Tactic:
rfl
State after:
no goals

State before:
case cons
α : Type u_1
head : α
tail : List α
⊢ head :: tail = head :: tail ++ []
Tactic:
simp only [append_nil]
State after:
no goals