intro n h
case cons
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {n : Nat}, n ≤ l.length → (take n l).length = n
⊢ ∀ {n : Nat}, n ≤ (t :: l).length → (take n (t :: l)).length = n
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