induction xs generalizing ys
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
xs : List α
ys : List β
h1 : v ∈ xs
h2 : f v = g v
⊢ updateListITE f xs ys v = updateListITE g xs ys v
case nil
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
h2 : f v = g v
ys : List β
h1 : v ∈ []
⊢ updateListITE f [] ys v = updateListITE g [] ys v

case cons
α β : Type
inst✝ : DecidableEq α
f g : α → β
v : α
h2 : f v = g v
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (ys : List β), v ∈ tail✝ → updateListITE f tail✝ ys v = updateListITE g tail✝ ys v
ys : List β
h1 : v ∈ head✝ :: tail✝
⊢ updateListITE f (head✝ :: tail✝) ys v = updateListITE g (head✝ :: tail✝) ys v