simp at h1
α β : Type
inst✝ : DecidableEq α
f : α → β
v : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∉ xs_tl → updateListITE f xs_tl ys v = f v
ys_hd : β
ys_tl : List β
h1 : v ∉ v :: xs_tl
⊢ ys_hd = f v
no goals