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