intro i hi
case cons
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {i : Nat}, i < l.length → (l.eraseIdx i).length = l.length - 1
⊢ ∀ {i : Nat}, i < (t :: l).length → ((t :: l).eraseIdx i).length = (t :: l).length - 1
case cons
α✝ : Type u_1
t : α✝
l : List α✝
ih : ∀ {i : Nat}, i < l.length → (l.eraseIdx i).length = l.length - 1
i : Nat
hi : i < (t :: l).length
⊢ ((t :: l).eraseIdx i).length = (t :: l).length - 1