cases ys
α β : Type
inst✝ : DecidableEq α
f : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∉ xs_tl → updateListITE f xs_tl ys v = f v
ys : List β
h1 : v ∉ xs_hd :: xs_tl
⊢ updateListITE f (xs_hd :: xs_tl) ys v = f v
case nil
α β : Type
inst✝ : DecidableEq α
f : α → β
v xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), v ∉ xs_tl → updateListITE f xs_tl ys v = f v
h1 : v ∉ xs_hd :: xs_tl
⊢ updateListITE f (xs_hd :: xs_tl) [] v = f v

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