case neg c1 =>
  simp at h2
  exact xs_ih ys_tl h1 h2
α β : Type
inst✝ : DecidableEq α
f g : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → xs_tl.length = ys.length → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
h2 : (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
h1 : v ∈ xs_tl
c1 : ¬v = xs_hd
⊢ updateListITE f xs_tl ys_tl v = updateListITE g xs_tl ys_tl v
no goals