case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
x : α
u : Fin m → α
i✝ : Unit
x✝ : Fin (Nat.succ m)
⊢ row (vecCons x u) i✝ x✝ = vecCons x u x✝
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
x : α
u : Fin m → α
⊢ row (vecCons x u) = fun x_1 => vecCons x u
ext
no goals
case a.h
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
x : α
u : Fin m → α
i✝ : Unit
x✝ : Fin (Nat.succ m)
⊢ row (vecCons x u) i✝ x✝ = vecCons x u x✝
rfl