∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] {W X Y Z : C} (h : W ⟶ Z) (x : X ⟶ W) (y : Y ⟶ W)
  (t : CategoryTheory.Limits.PullbackCone x y),
  CategoryTheory.CategoryStruct.comp t.fst (CategoryTheory.CategoryStruct.comp x h) =
    CategoryTheory.CategoryStruct.comp t.snd (CategoryTheory.CategoryStruct.comp y h)