apply Function.updateITE_comp_left
α β γ : 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_hd : β
ys_tl : List β
⊢ g ∘ updateITE (updateListITE f xs_tl ys_tl) xs_hd ys_hd = updateITE (g ∘ updateListITE f xs_tl ys_tl) xs_hd (g ys_hd)
no goals