∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject C}
  (s : SimplicialObject.Splitting X) [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {Δ : SimplexCategoryᵒᵖ}
  (A B : SimplicialObject.Splitting.IndexSet Δ),
  B ≠ A → CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) (s.πSummand B) = 0