English
If two arrows f,g : α ⟹ β satisfy dropFun f = dropFun g and lastFun f = lastFun g, then f = g. An arrow is determined by its prefix and last coordinate.
Русский
Если две стрелы f,g : α ⟹ β удовлетворяют dropFun f = dropFun g и lastFun f = lastFun g, то f = g. Стрела определяется префиксом и последней координатой.
LaTeX
$$$\forall \{n\},\ \forall \alpha,\beta:\mathrm{TypeVec}(n+1),\ \forall f,g:\alpha \Rightarrow \beta,\ (\mathrm{dropFun} f=\mathrm{dropFun} g) \to (\mathrm{lastFun} f=\mathrm{lastFun} g) \to f=g$$$
Lean4
theorem eq_of_drop_last_eq {α β : TypeVec (n + 1)} {f g : α ⟹ β} (h₀ : dropFun f = dropFun g)
(h₁ : lastFun f = lastFun g) : f = g := by
refine funext (fun x => ?_)
cases x
· apply h₁
· apply congr_fun h₀
