chore(algebraic_topology/simplex_category): golf proof (#8076)
The "special case of the first simplicial identity" is a trivial consequence of the "generic case". This makes me wonder whether the special case should be there at all but I do not know the standard references for this stuff.
