have t := hk (tw_inj n 1 h')
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 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
t : False
⊢ False