∀ {X : SSet} (f₀ f₂ f₃ : SSet.stdSimplex.obj (SimplexCategory.mk 2) ⟶ X)
  (h₁₂ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₃)
  (h₁₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 1) f₀ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) f₂)
  (h₂₃ :
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₂ =
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 2) f₃),
  (SSet.horn₃₁.desc.multicofork f₀ f₂ f₃ h₁₂ h₁₃ h₂₃).π ⟨2, SSet.horn₃₁.desc.multicofork_π_two._proof_1⟩ =
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonComplIso 2).inv f₂