∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C}
  (s : SimplicialObject.Splitting X) {Δ₁ Δ₂ : SimplexCategoryᵒᵖ} (A : SimplicialObject.Splitting.IndexSet Δ₁)
  (p : Δ₁ ⟶ Δ₂) [inst_1 : CategoryTheory.Epi p.unop] {Z : C} (h : X.obj Δ₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((s.cofan Δ₁).inj A) (CategoryTheory.CategoryStruct.comp (X.map p) h) =
    CategoryTheory.CategoryStruct.comp ((s.cofan Δ₂).inj (A.epiComp p)) h