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