∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S₁ S₂ : SimplicialObject.Split C} (Φ : S₁ ⟶ S₂)
  {Δ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ) {Z : C} (h : S₂.X.obj Δ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((S₁.s.cofan Δ).inj A) (CategoryTheory.CategoryStruct.comp (Φ.F.app Δ) h) =
    CategoryTheory.CategoryStruct.comp (Φ.f (Opposite.unop A.fst).len)
      (CategoryTheory.CategoryStruct.comp ((S₂.s.cofan Δ).inj A) h)