decide whether renamings of dfss2 and others are provisional

[wlammen]

This pull request is a reminder that some renamings in #4840 were disputed, and hence marked as provisional.

It may stay open until a final decision is made. Depending on the outcome it either gets merged, or declined and a different pull request reverts some or all renamings.

This pull request does not aim at urging a decision making, and so may stay open as long as it takes. The comment section may serve as a discussion platform.

[wlammen]

Copied from #4840, a remark from @avekens :

I think we should NOT rename these theorems, at least not in this proposed way. It should still be clear in the future that ~dfss2 was/could be an alternate definition. And why should the other alternate definitions should just be renumbered, and not renamed accordingly?
The only theorem which may be renamed is ~dfss: it is just the commuted form of ~dfss2, so maybe it should be called ~dfss2c.