∀ {n : ℕ} (X : SSet.Truncated (n + 1)) (m : ℕ) (h : m ≤ n + 1)
  (Δ : X.obj (Opposite.op { obj := SimplexCategory.mk m, property := h })) (i : Fin m),
  ((SSet.Truncated.trunc (n + 1) 1 ⋯).obj X).map
      (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ 1) SSet.Truncated.Path₁._proof_1
          SSet.Truncated.Path₁._proof_5).op
      (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.mkOfSucc i) ⋯ h).op Δ) =
    X.map (SimplexCategory.Truncated.Hom.tr ((SimplexCategory.mk 0).const (SimplexCategory.mk m) i.castSucc) ⋯ h).op Δ