∀ {n : ℕ} (S : Finset (Fin (n + 1))) {d : ℕ}
  (x : (SSet.stdSimplex.obj (SimplexCategory.mk n)).obj (Opposite.op (SimplexCategory.mk d))),
  (x ∈ (SSet.stdSimplex.face S).obj (Opposite.op (SimplexCategory.mk d))) = ∀ (i : Fin (d + 1)), x i ∈ S