case h
α : Type u
m n o : ℕ
m' : Type ?u.27911
n' : Type ?u.27914
o' : Type ?u.27917
v : Fin n → α
x✝ : Fin n
⊢ vecAppend (_ : n = 0 + n) ![] v x✝ = v x✝
α : Type u
m n o : ℕ
m' : Type ?u.27911
n' : Type ?u.27914
o' : Type ?u.27917
v : Fin n → α
⊢ vecAppend (_ : n = 0 + n) ![] v = v
ext
no goals
case h
α : Type u
m n o : ℕ
m' : Type ?u.27911
n' : Type ?u.27914
o' : Type ?u.27917
v : Fin n → α
x✝ : Fin n
⊢ vecAppend (_ : n = 0 + n) ![] v x✝ = v x✝
simp [vecAppend_eq_ite]