{ rintro ⟨i, rfl⟩; cases i using Fin.cases <;> simp }
case succ.mpr
α : Type u_1
a : α
n✝ : ℕ
a✝ : ∀ {v : Fin n✝ → α}, a ∈ toList v ↔ ∃ i, v i = a
v : Fin (n✝ + 1) → α
⊢ (∃ i, v i = a) → a = v 0 ∨ ∃ i, v i.succ = a
no goals