Hillel,
I feel that the “Weak” fairness implies the existence of “strong” fairness. may introduce bit confusion to beginners.
I mean, the "imply" word could make people get confused. I don't think you want to say:
WF implies SF, which means: WF(A) --> SF(A). However, from TLA+, It should be otherwise. I mean, SF(A)-->WF(A).
I guess you just wanted to tell readers that the "existence of SF". So, maybe we don't want to use "implies" word here, which is more a reserved word for prepositional logic.
Best regards,
Michael