simp
case pos
α β : Type
inst✝ : DecidableEq α
a b c : α
d : β
f : α → α
g : α → β
h1 : f a = c → d = g (f a)
c1 : a = b
⊢ (if (if True then c else f b) = c then d else g (if True then c else f b)) = if True then d else (g ∘ f) b
no goals