no goals
α : Type u
o n m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
a b : ℕ
v : n' → α
B : Fin m → n' → α
i : Fin (Nat.succ m)
j : n'
⊢ vecCons v B i j = vecCons (v j) (fun i => B i j) i
refine' Fin.cases _ _ i <;> simp