cases n with
| zero => simp
| succ n => simp [ih (by rw [length_cons, succ_le_succ_iff] at h; exact h)]
case cons
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {n : Nat}, n ≤ l.length → (take n l).length = n
n : Nat
h : n ≤ (t :: l).length
⊢ (take n (t :: l)).length = n
no goals