∀ {X : SSet} {A : X.Subcomplex} (toN toN_1 : X.N) (e_toN : toN = toN_1)
  (notMem : toN.simplex ∉ A.obj (Opposite.op (SimplexCategory.mk toN.dim))),
  { toN := toN, notMem := notMem } = { toN := toN_1, notMem := ⋯ }