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

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