exact (h' k hjk).symm
case neg
n✝ n : ℕ
a : ↑(testvecs n 1)
h₂ : ∑ k : Fin (Nat.succ n), ↑a k = 1
j : Fin (Nat.succ n)
hj : ↑a j = 1
h' : ∀ (k : Fin (Nat.succ n)), k ≠ j → ↑a k = 0
k : Fin (Nat.succ n)
hjk : ¬k = j
⊢ 0 = ↑a k
no goals