simp only [take, length]
α : Type u_1
n : Nat
x : α
xs : List α
h : Nat.succ n < length (x :: xs)
ih : length (take n xs) = n
⊢ length (take (Nat.succ n) (x :: xs)) = Nat.succ n
α : Type u_1
n : Nat
x : α
xs : List α
h : Nat.succ n < length (x :: xs)
ih : length (take n xs) = n
⊢ length (take n xs) + 1 = Nat.succ n