English
Let α be a vector of length n and p be a binary relation on β. There is a predicate on the product of two copies of the vector, depending only on their last coordinates: it holds for ((a1,...,an,b),(a1',...,an',b')) iff the first n coordinates coincide and p(b,b').
Русский
Пусть α — вектор типов длины n, и p — бинарное отношение на β. Существует предикат на произведении двух копий вектора, зависящий только от последних координат: он выполняется для ((a1,...,an,b),(a1',...,an',b')) тогда, когда первые n координат совпадают и выполняется p(b,b').
LaTeX
$$$RelLast'(\\alpha,p)((a_1,...,a_n,b),(a_1',...,a_n',b')) \\iff (a_1,...,a_n) = (a_1',...,a_n') \\land p(b,b').$$$
Lean4
/-- predicate on the product of two type vectors to constrain only their last object -/
def RelLast' (α : TypeVec n) {β : Type*} (p : β → β → Prop) : (α ::: β) ⊗ (α ::: β) ⟹ «repeat» (n + 1) Prop :=
splitFun (repeatEq α) (uncurry p)
