∀ {α : Type u_1} {n : ℕ} {p : α → Prop} {xs : Vector { x // p x } n} {f : { x // p x } → Bool} {g : α → Bool},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → Vector.findFinIdx? f xs = Vector.findFinIdx? g xs.unattach