English
For any β on 0-length TypeVec, and any f in β(nilFun), there is a canonical way to assign to every v ∈ TypeVec(0) an element of β v, obtained by transporting f along the unique equality v = nilFun.
Русский
Для любого β над нулевой длиной TypeVec и любого f ∈ β(nilFun) существует канонический способ задать для каждого v ∈ TypeVec(0) элемент β v, полученный транспортом f вдоль единственного равенства v = nilFun.
LaTeX
$$$$\\mathrm{casesNil}: (\\beta: \\text{TypeVec}(0) \\to \\text{Sort}) \\to \\beta(\\mathrm{nilFun}) \\to \\forall v, \\beta(v).$$$$
Lean4
/-- cases distinction for 0-length type vector -/
protected def casesNil {β : TypeVec 0 → Sort*} (f : β Fin2.elim0) : ∀ v, β v := fun v =>
cast (by congr; funext i; cases i) f
