no goals
C : Type u
inst✝¹ : Category C
X✝ Y✝ Z✝ : C
P : Prop
inst✝ : Decidable P
X Y Z : C
f : P → (X ⟶ Y)
f' : ¬P → (X ⟶ Y)
g : Y ⟶ Z
⊢ (if h : P then f h else f' h) ≫ g = if h : P then f h ≫ g else f' h ≫ g
aesop