simp only [Function.updateListITE]
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
ys : List α
⊢ updateListITE f [] (List.map f ys) x = updateListITE g [] (List.map f ys) x
α β : Type
inst✝ : DecidableEq α
f g : α → β
x : α
h1 : f x = g x
ys : List α
⊢ f x = g x