∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op (SimplexCategory.mk 0))} {f g fg : X.PtSimplex n x} {i : Fin n}
  (self : f.MulStruct g fg i) (j : Fin (n + 2)),
  i.succ.succ < j → CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ j) self.map = SSet.const x