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

State before:
α✝ : Type u_1
x : α✝
xs : List α✝
⊢ length (x :: xs) = succ (length xs)
Tactic:
simp
State after:
no goals