∀ {S : SSet} {n : ℕ} {j : Fin (n + 2)} {i : Fin (n + 1)},
  j = i.succ →
    ∀ (x : S.obj (Opposite.op (SimplexCategory.mk n))),
      CategoryTheory.SimplicialObject.δ S j (CategoryTheory.SimplicialObject.σ S i x) = x