English
A specialised case distinction for arrows in the category of 0-length vectors: one can evaluate the arrow only at Fin2.elim0 and transport across equalities to any v,v',fs.
Русский
Специализированное распознавание случаев для стрелок в категории нулевой длины векторов: стрелку можно рассмотреть только в Fin2.elim0 и перенести вдоль равенств на любые v, v', fs.
LaTeX
$$$$\\forall (β: \\forall v v': TypeVec(0), v \\Rightarrow v' \\to \\text{Sort}) (f: β(\\mathrm{Fin2}.elim0, \\mathrm{Fin2}.elim0, \\mathrm{TypeVec}.nilFun)), \\forall v v' fs, β v v' fs.$$$$
Lean4
protected theorem casesNil_append1 {β : TypeVec 0 → Sort*} (f : β Fin2.elim0) : TypeVec.casesNil f Fin2.elim0 = f :=
rfl
