This discussion has been a bit spread across a few issues and pull
requests, so it seems good to offer a message here about the rename
underway to some of the theorems with "syl" in their names. There is a
list of all the theorems affected here:
https://github.com/metamath/set.mm/blob/develop/changes-set.txt#L35 .
I'm starting with the syl5 ones.
Because each of these pull requests (two have been merged so far) touch
a lot of lines, it probably is better to merge them quickly rather than
leave a lot of time between approval and merging, so if you see any
proposed renames in the above list which you think should be changed or
considered at more length, speak up now (here on the mailing list, make
a github issue, make a pull request to the change-set.txt file, etc).