induction n <;> simp[*]
α : Type u_1
n : ℕ
v : Fin n → α
a : α
⊢ a ∈ toList v ↔ ∃ i, v i = a
case succ
α : Type u_1
a : α
n✝ : ℕ
a✝ : ∀ {v : Fin n✝ → α}, a ∈ toList v ↔ ∃ i, v i = a
v : Fin (n✝ + 1) → α
⊢ (a = v 0 ∨ ∃ i, v i.succ = a) ↔ ∃ i, v i = a