case a.h
n : ℕ
α : TypeVec 0
β : TypeVec 0
f : α ⟹ β
x : Fin2 0
x✝ : α x
⊢ f x x✝ = nilFun x x✝
n : ℕ
α : TypeVec 0
β : TypeVec 0
f : α ⟹ β
⊢ f = nilFun
ext x
no goals
case a.h
n : ℕ
α : TypeVec 0
β : TypeVec 0
f : α ⟹ β
x : Fin2 0
x✝ : α x
⊢ f x x✝ = nilFun x x✝
cases x