simp only [Function.updateListITE]
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
⊢ updateListITE f (hd :: tl) (g hd :: List.map g tl) x = g x
α β : Type
inst✝ : DecidableEq α
f g : α → β
x hd : α
tl : List α
ih : x ∈ tl → updateListITE f tl (List.map g tl) x = g x
h1 : x = hd ∨ x ∈ tl
⊢ updateITE (updateListITE f tl (List.map g tl)) hd (g hd) x = g x