no goals
α : Type u
m n o : ℕ
m' : Type ?u.78559
n' : Type ?u.78562
o' : Type ?u.78565
inst✝ : Zero α
v : Fin n → α
x : α
h : vecCons x v = 0
⊢ v = 0
convert congr_arg vecTail h
no goals
α : Type u
m n o : ℕ
m' : Type ?u.78559
n' : Type ?u.78562
o' : Type ?u.78565
inst✝ : Zero α
v : Fin n → α
x : α
x✝ : x = 0 ∧ v = 0
hx : x = 0
hv : v = 0
⊢ vecCons x v = 0
simp [hx, hv]