split_ifs with h'
case neg
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
hk : ¬k = 0
⊢ 1 = if tw n 1 k = tw n 1 0 then 0 else 1
case pos
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
hk : ¬k = 0
h' : tw n 1 k = tw n 1 0
⊢ False

case neg
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
hk : ¬k = 0
h' : ¬tw n 1 k = tw n 1 0
⊢ 1 = 1