cases i using Fin.cases <;> simp[ha, hv]
case intro.intro.intro.intro
α : Type u_1
n : ℕ
v✝ : Fin (n + 1) →. α
a : α
ha : a ∈ v✝ 0
v : Vector α n
hv : ∀ (i : Fin n), v.get i ∈ v✝ i.succ
i : Fin (n + 1)
⊢ (a ::ᵥ v).get i ∈ v✝ i
no goals