case cons xs_hd xs_tl xs_ih =>
  cases ys
  case nil =>
    simp only [Function.updateListITE]
    simp only [Function.updateITE]
    simp only [if_neg h1]
  case cons ys_hd ys_tl =>
    simp only [Function.updateListITE]
    simp only [Function.updateITE]
    split_ifs
    case pos c1 =>
      rfl
    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 : List β
⊢ updateListITE (updateITE f y z) (xs_hd :: xs_tl) ys x = updateListITE f (xs_hd :: xs_tl) ys x
no goals