exact ⟨w.head, by simpa using h 0, w.tail, fun i => by simpa using h i.succ, by simp⟩
α : Type u_1
n : ℕ
w : Vector α (n + 1)
v : Fin (n + 1) →. α
h : ∀ (i : Fin (n + 1)), w.get i ∈ v i
⊢ ∃ a ∈ v 0, ∃ a_1, (∀ (i : Fin n), a_1.get i ∈ v i.succ) ∧ w = a ::ᵥ a_1
no goals