simp[Vector.mOfFn, @mem_vector_mOfFn _ n]
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
⊢ w ∈ Vector.mOfFn v ↔ ∀ (i : Fin (n + 1)), w.get i ∈ v i
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
⊢ (∃ a ∈ v 0, ∃ a_1, (∀ (i : Fin n), a_1.get i ∈ v i.succ) ∧ w = a ::ᵥ a_1) ↔ ∀ (i : Fin (n + 1)), w.get i ∈ v i