rw [length_cons, succ_le_succ_iff] at h
α✝ : 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
⊢ ?m.37095 ≤ l.length
α✝ : 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
h : n ≤ l.length
⊢ ?m.37095 ≤ l.length