simp at h1
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
h2 : f v = g v
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
h1 : v ∈ xs_hd :: xs_tl
ys_hd : β
ys_tl : List β
⊢ updateListITE f (xs_hd :: xs_tl) (ys_hd :: ys_tl) v = updateListITE g (xs_hd :: xs_tl) (ys_hd :: ys_tl) v
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
h2 : f v = g v
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∈ xs_tl → updateListITE f xs_tl ys v = updateListITE g xs_tl ys v
ys_hd : β
ys_tl : List β
h1 : v = xs_hd ∨ v ∈ xs_tl
⊢ updateListITE f (xs_hd :: xs_tl) (ys_hd :: ys_tl) v = updateListITE g (xs_hd :: xs_tl) (ys_hd :: ys_tl) v