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

State before:
α : Type u_1
n : ℕ
x : α
xs : List α
⊢ take (n + 1) (x :: xs) = x :: take n xs
Tactic:
rw [take]
State after:
no goals