case neg c1 =>
  apply xs_ih
α β : Type
inst✝ : DecidableEq α
f : α → β
x y : α
z : β
h1 : ¬x = y
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), updateListITE (updateITE f y z) xs_tl ys x = updateListITE f xs_tl ys x
ys_hd : β
ys_tl : List β
c1 : ¬x = xs_hd
⊢ updateListITE (updateITE f y z) xs_tl ys_tl x = updateListITE f xs_tl ys_tl x
no goals