English
Specialized cases distinction for an arrow in the category of 0-length TypeVec arrows: any two arrows with nilFun components coincide.
Русский
Специализированное разделение случаев для стрелки в категории стрелок нулевой длины TypeVec: любые две стрелки с компонентами nilFun совпадают.
LaTeX
$$$$\\forall β, g: β\\ (nilFun) \\Rightarrow g = nilFun.$$$$
Lean4
/-- cases distinction for an arrow in the category of (n+1)-length type vectors -/
def typevecCasesCons₃ (n : ℕ) {β : ∀ v v' : TypeVec (n + 1), v ⟹ v' → Sort*}
(F : ∀ (t t') (f : t → t') (v v' : TypeVec n) (fs : v ⟹ v'), β (v ::: t) (v' ::: t') (fs ::: f)) :
∀ v v' fs, β v v' fs := by
intro v v'
rw [← append1_drop_last v, ← append1_drop_last v']
intro fs
rw [← split_dropFun_lastFun fs]
apply F
