∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
  (s : CategoryTheory.Limits.Trident f) (j : J) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (s.π.app CategoryTheory.Limits.WalkingParallelFamily.zero)
      (CategoryTheory.CategoryStruct.comp (f j) h) =
    CategoryTheory.CategoryStruct.comp (s.π.app CategoryTheory.Limits.WalkingParallelFamily.one) h