no goals
C✝ : Type u
inst✝² : Category C✝
X✝ Y✝ : C✝
C : Type u
inst✝¹ : Category C
V W X Y : C
inst✝ : HasBinaryCoproduct X Y
f : V ⟶ W
g : X ⟶ V
h : Y ⟶ V
Z : C
l : W ⟶ Z
⊢ desc g h ≫ f ≫ l = desc (g ≫ f) (h ≫ f) ≫ l
simp