∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {B X : C} (f : X ⟶ B)
  (c : CategoryTheory.Limits.PullbackCone f f) (hc : CategoryTheory.Limits.IsLimit c)
  (s : CategoryTheory.Limits.Cocone (CategoryTheory.Limits.parallelPair c.fst c.snd)) {Z : C} (g₁ g₂ : Z ⟶ X),
  CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
    CategoryTheory.CategoryStruct.comp g₁ (s.ι.app CategoryTheory.Limits.WalkingParallelPair.one) =
      CategoryTheory.CategoryStruct.comp g₂ (s.ι.app CategoryTheory.Limits.WalkingParallelPair.one)