rw [take_cons_succ]
case cons
α : Type u_1
a : α
as : List α
ih : take as.length as = as
⊢ take as.length.succ (a :: as) = a :: as
case cons
α : Type u_1
a : α
as : List α
ih : take as.length as = as
⊢ a :: take as.length as = a :: as