induction xs generalizing ys
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
xs : List α
ys : List β
⊢ g ∘ updateListITE f xs ys = updateListITE (g ∘ f) xs (List.map g ys)
case nil
α β γ : Type
inst✝ : DecidableEq α
f : α → β
g : β → γ
ys : List β
⊢ g ∘ updateListITE f [] ys = updateListITE (g ∘ f) [] (List.map g ys)

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