rw [ih hi, Nat.sub_add_cancel (zero_lt_of_lt hi)]
case cons.succ
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {i : Nat}, i < l.length → (l.eraseIdx i).length = l.length - 1
i : Nat
hi : i < l.length
⊢ (l.eraseIdx i).length + 1 = l.length
no goals