case cons hd tl ih =>
  simp at h1
  push_neg at h1
  cases h1
  case intro h1_left h1_right =>
    simp
    simp only [Function.updateITE]
    split_ifs <;> tauto
α β : Type
inst✝ : DecidableEq α
f : α → β
a : α
b : β
hd : α
tl : List α
ih : a ∉ tl → List.map (updateITE f a b) tl = List.map f tl
h1 : a ∉ hd :: tl
⊢ List.map (updateITE f a b) (hd :: tl) = List.map f (hd :: tl)
no goals