case cons xs_hd xs_tl xs_ih =>
  cases ys
  case nil =>
    simp only [Function.updateListITE]
  case cons ys_hd ys_tl =>
    simp only [Function.updateListITE]
    simp only [Function.updateITE]
    split_ifs
    case pos c1 =>
      subst c1
      simp at h1
    case neg c1 =>
      simp at h1
      push_neg at h1
      cases h1
      case intro h1_left h1_right =>
        apply xs_ih ys_tl h1_right
α β : Type
inst✝ : DecidableEq α
f : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∉ xs_tl → updateListITE f xs_tl ys v = f v
ys : List β
h1 : v ∉ xs_hd :: xs_tl
⊢ updateListITE f (xs_hd :: xs_tl) ys v = f v
no goals