∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.ObjectProperty C) {X : C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct (P.coproductFromFamily X)] {Y : C} (f f_1 : Y ⟶ X),
  f = f_1 → ∀ (hY : P Y), P.ιCoproductFrom f hY = P.ιCoproductFrom f_1 hY