English
"Curried" exists: VectorEx k f holds iff f is satisfied by currying over k elements; defined by recursion on k with Vector3 α k.
Русский
"Каррированный" экзистенс: VectorEx k f определяется рекурсивно по k, с учётом векторной структуры Vector3 α k.
LaTeX
$$$ \mathrm{VectorEx} : \forall k, (\mathrm{Vector3}(\alpha,k) \to \mathrm{Prop}) \to \mathrm{Prop}, \\ \mathrm{VectorEx}\ 0\ f = f([]), \\ \mathrm{VectorEx}\ (\mathrm{succ}\ k)\ f = \exists x:\alpha, \mathrm{VectorEx}\ k\ (\lambda v. f(x :: v)). $$$
Lean4
/-- "Curried" exists, i.e. `∃ x₁ ... xₙ, f [x₁, ..., xₙ]`. -/
def VectorEx : ∀ k, (Vector3 α k → Prop) → Prop
| 0, f => f []
| succ k, f => ∃ x : α, VectorEx k fun v => f (x :: v)
