exact funext (fun i => i.cases (by simp[Matrix.empty_eq]) (by simp[Matrix.empty_eq]))
case succ
n n✝ : ℕ
a✝ : ∀ (v : Fin n✝ → ℕ), unvector (vecToNat v) = v
v : Fin (n✝ + 1) → ℕ
⊢ v 0 :> v ∘ Fin.succ = v
no goals