case nil =>
  simp only [Function.updateListITE]
  simp only [Function.updateITE]
  simp only [if_neg h1]
α β : Type
inst✝ : DecidableEq α
f : α → β
x y : α
z : β
h1 : ¬x = y
ys : List β
⊢ updateListITE (updateITE f y z) [] ys x = updateListITE f [] ys x
no goals