cases ys
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
ys : List β
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) ys = updateListITE (g ∘ f) (xs_hd :: xs_tl) (List.map g ys)
case nil
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) [] = updateListITE (g ∘ f) (xs_hd :: xs_tl) (List.map g [])

case cons
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs_hd : α
xs_tl : List α
xs_ih : ∀ (ys : List β), g ∘ updateListITE f xs_tl ys = updateListITE (g ∘ f) xs_tl (List.map g ys)
head✝ : β
tail✝ : List β
⊢ g ∘ updateListITE f (xs_hd :: xs_tl) (head✝ :: tail✝) =
    updateListITE (g ∘ f) (xs_hd :: xs_tl) (List.map g (head✝ :: tail✝))