case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
i✝ : Unit
x✝ : Fin 0
⊢ row ![] i✝ x✝ = ![]
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
⊢ row ![] = fun x => ![]
ext
no goals
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
i✝ : Unit
x✝ : Fin 0
⊢ row ![] i✝ x✝ = ![]
rfl