no goals
α : Type u_1
β : Type u_2
n : ℕ
a a' : α
b : β
v : Vector α (n + 1)
f : α → β
⊢ b ∈ toList (map f v) ↔ f (head v) = b ∨ ∃ a, a ∈ toList (tail v) ∧ f a = b
rw [mem_succ_iff, head_map, tail_map, mem_map_iff, @eq_comm _ b]