English
A general form of case distinction for arrows between (n+1)-length TypeVecs, lifting a function F that handles (t ::: v) cases to arbitrary v and fs through reindexing.
Русский
Обобщённая форма разбиения по случаям стрелок между векторами длины (n+1), поднимающая функцию F, обрабатывающую случаи (t ::: v) к произвольным v и fs через перенумерацию.
LaTeX
$$$$\\text{typevecCasesCons₃}(n)(F)(v)(v')(fs) = F\\, (v ::: t) (v' ::: t') (fs ::: f).$$$$
Lean4
/-- specialized cases distinction for an arrow in the category of (n+1)-length type vectors -/
def typevecCasesCons₂ (n : ℕ) (t t' : Type*) (v v' : TypeVec n) {β : (v ::: t) ⟹ (v' ::: t') → Sort*}
(F : ∀ (f : t → t') (fs : v ⟹ v'), β (fs ::: f)) : ∀ fs, β fs :=
by
intro fs
rw [← split_dropFun_lastFun fs]
apply F
