∀ {n d : ℕ} (s : (SSet.stdSimplex.obj (SimplexCategory.mk n)).obj (Opposite.op (SimplexCategory.mk d))),
  (s ∈ (SSet.stdSimplex.obj (SimplexCategory.mk n)).nonDegenerate d) = CategoryTheory.Mono (SSet.stdSimplex.objEquiv s)