English
PredLast defines, for a fixed vector α and predicate p on β, a predicate on α.append1 β which depends only on the last coordinate: the last coordinate obeys p, all earlier coordinates are unconstrained.
Русский
PredLast задаёт предикат на α ⧺ β, который зависит только от последнего координата: для последнего элемента выполняется p, остальные свободны.
LaTeX
$$$$\\mathrm{PredLast}(\\alpha)(p) : \\forall i, (\\alpha\\append1 \\beta) i \\to \\mathrm{Prop}, \\; (i=\\mathrm{fz}) \\Rightarrow p, \\; (i=\\mathrm{fs}) \\Rightarrow \\mathrm{True}.$$$$
Lean4
/-- `PredLast α p x` predicates `p` of the last element of `x : α.append1 β`. -/
def PredLast (α : TypeVec n) {β : Type*} (p : β → Prop) : ∀ ⦃i⦄, (α.append1 β) i → Prop
| Fin2.fs _ => fun _ => True
| Fin2.fz => p
