∀ {X : SSet.Truncated 2}
  {x₀ x₁ : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := SSet.Truncated.Edge._proof_1 })}
  (self : SSet.Truncated.Edge x₀ x₁),
  X.map (SimplexCategory.Truncated.δ₂ 1 SSet.Truncated.Edge._proof_1 SSet.Truncated.Edge._proof_3).op self.edge = x₀