English
RelLast describes when the last elements of two vectors are related by a relation r, while all other components are equal, i.e., only the last coordinate carries the relation.
Русский
RelLast описывает, когда последние элементы двух векторов связаны отношением r, все остальные координаты равны, то есть только последняя координата несёт отношение.
LaTeX
$$$$\\mathrm{RelLast}(\\alpha)(r) : \\forall i, (\\alpha.append1 β) i \\to (\\alpha.append1 γ) i \\to \\text{Prop}, \\; (i = \\mathrm{fs})->Eq, (i=\\mathrm{fz})-> r.$$$$
Lean4
/-- `RelLast α r x y` says that `p` the last elements of `x y : α.append1 β` are related by `r` and
all the other elements are equal. -/
def RelLast (α : TypeVec n) {β γ : Type u} (r : β → γ → Prop) : ∀ ⦃i⦄, (α.append1 β) i → (α.append1 γ) i → Prop
| Fin2.fs _ => Eq
| Fin2.fz => r
