induction l with
| nil => simp
| cons t l ih =>
  intro i hi
  cases i with
  | zero => simp
  | succ i =>
    simp
    rw [length_cons, succ_lt_succ_iff] at hi
    rw [ih hi, Nat.sub_add_cancel (zero_lt_of_lt hi)]
α✝ : Type u_1
l : List α✝
⊢ ∀ {i : Nat}, i < l.length → (l.eraseIdx i).length = l.length - 1
no goals