rw [ha.symm, pair_tw, Nat.sub_self, zero_mul, zero_add, w1_apply]
case intro
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
⊢ pair (w1 n) ↑a = if a = tw n 1 0 then 0 else 1
case intro
n✝ n : ℕ
inst✝¹ : NeZero n
inst✝ : DecidableEq ↑(testvecs n 1)
a : ↑(testvecs n 1)
k : Fin (Nat.succ n)
ha : tw n 1 k = a
⊢ (if k = 0 then 0 else 1) = if tw n 1 k = tw n 1 0 then 0 else 1