case a.h
n : ℕ
α : TypeVec 0
i : Fin2 0
x✝ : (α ⊗ α) i
⊢ repeatEq α i x✝ = nilFun i x✝
n : ℕ
α : TypeVec 0
⊢ repeatEq α = nilFun
ext i
no goals
case a.h
n : ℕ
α : TypeVec 0
i : Fin2 0
x✝ : (α ⊗ α) i
⊢ repeatEq α i x✝ = nilFun i x✝
cases i