simp
case h
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
⊢ (updateITE g a b ∘ f) x = updateITE (g ∘ f) (finv a) b x
case h
α β γ : Type
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finv : β → α
g : β → γ
a : β
b : γ
h1 : finv ∘ f = id
h2 : f ∘ finv = id
x : α
⊢ updateITE g a b (f x) = updateITE (g ∘ f) (finv a) b x