simp
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 + 1 < (t :: l).length
⊢ ((t :: l).eraseIdx (i + 1)).length = (t :: l).length - 1
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 + 1 < (t :: l).length
⊢ (l.eraseIdx i).length + 1 = l.length