English
For predicates on vectors of length n+1, existence of a witness is equivalent to the existence of a head and a tail, i.e., there exist x in α and v in Vector3 α n with f(x :: v).
Русский
Для предикатов над векторами длины n+1 существование вектора, удовлетворяющего предикату, эквивалентно существованию головой и хвостом: существует x ∈ α и v ∈ Vector3 α n such that f(x :: v).
LaTeX
$$$(\exists f : Vector3(\alpha,\mathrm{succ} n) \to \mathrm{Prop})\; \Rightarrow \; (\exists x:\alpha)(\exists v:\ Vector3(\alpha,n),\; f(x::v)).$$$
Lean4
theorem exists_vector_succ (f : Vector3 α (succ n) → Prop) : Exists f ↔ ∃ x v, f (x :: v) :=
⟨fun ⟨v, fv⟩ => ⟨_, _, by rw [cons_head_tail v]; exact fv⟩, fun ⟨_, _, fxv⟩ => ⟨_, fxv⟩⟩
