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