It is be interesting to think of how a checker would work that detects monotonicity & deploys this theorem to check liveness properties. Maybe I'm just describing the TLA+ proof language! Also something to bring up at the next monthly TLA+ meeting.