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

State before:
α : Type u_1
x : α
xs ys : List α
⊢ x :: (xs ++ ys) = x :: xs ++ ys
Tactic:
apply (congrArg (cons x))
State after:
α : Type u_1
x : α
xs ys : List α
⊢ xs ++ ys = List.append xs ys

State before:
α : Type u_1
x : α
xs ys : List α
⊢ xs ++ ys = List.append xs ys
Tactic:
rfl
State after:
no goals