English
Let α be a vector of types of length n and let p be a predicate on a type β. There exists a predicate on the extended vector α ::: β that depends only on the last component: it holds for a tuple (a1, a2, ..., an, b) iff p(b).
Русский
Пусть α задаёт вектор типов длины n, и пусть p — предикат на β. Существует предикат на расширенный вектор α ::: β, который зависит только от последнего элемента: он выполняется для кортежа (a1, a2, ..., an, b) тогда и только тогда, когда выполняется p(b).
LaTeX
$$$PredLast'(\\alpha,p)((a_1, \\dots, a_n, b)) \\iff p(b).$$$
Lean4
/-- predicate on a type vector to constrain only the last object -/
def PredLast' (α : TypeVec n) {β : Type*} (p : β → Prop) : (α ::: β) ⟹ «repeat» (n + 1) Prop :=
splitFun (TypeVec.const True α) p
