∀ {α : Type u_1} {n : ℕ} {a : α} {xs : Vector α n} (motive : (∃ i, ∃ (h : i < n), xs[i] = a) → Prop)
  (x : ∃ i, ∃ (h : i < n), xs[i] = a), (∀ (n_1 : ℕ) (w : n_1 < n) (e : xs[n_1] = a), motive ⋯) → motive x