have s1 : ∀ (y : α), y ∈ ys → f y =Function.updateITE f v a y
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map (updateITE f v a) ys) x
case s1
α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
⊢ ∀ y ∈ ys, f y = updateITE f v a y

α β : Type
inst✝ : DecidableEq α
f g : α → β
xs ys : List α
v : α
a : β
x : α
h1 : ∀ y ∈ ys, ¬y = v
h2 : xs.length = ys.length
h3 : x ∈ xs
s1 : ∀ y ∈ ys, f y = updateITE f v a y
⊢ updateListITE f xs (List.map f ys) x = updateListITE g xs (List.map (updateITE f v a) ys) x