case a
n : ℕ
β : Type u_1
x : β
α : TypeVec 0
i : Fin2 0
⊢ TypeVec.const x α i = nilFun i
n : ℕ
β : Type u_1
x : β
α : TypeVec 0
⊢ TypeVec.const x α = nilFun
ext i : 1
no goals
case a
n : ℕ
β : Type u_1
x : β
α : TypeVec 0
i : Fin2 0
⊢ TypeVec.const x α i = nilFun i
cases i