Add leadsTo and fix fairness effects

[bugarela]

Hello

We were missing one temporal operator for no reason, leadsTo (or ~> in TLA+). This adds that, as this felt too big of a shame now that we support TLC. We also need to add the transpilation on Apalache side, so this is blocked by that (I have the change and will open a PR there soon).

I also fixed one bug where Quint would complain about the effects of weakFair and strongFair in some scenarios. The effect was wrong, but the infrastructure for effects made it not so trivial to fix it. I ended up updating the effect parser to allow for a smooth change that keeps the nice format of the effect signatures (without needing to define the signature manually for this special case).

• I have read and I understand the Note on AI-assisted contributions
• Changes manually tested locally and confirmed to work as described
  (including screenshots is helpful)
• Tests added for any new code
• Documentation added for any new functionality
• Entries added to the respective CHANGELOG.md for any new functionality

[bugarela]

I don't think we ever want to support this. I'd much rather have people always add the fairness assumptions to the properties. It's a nightmare to explain that we have an alternative to init and step with spec that takes a temporal formula, blabla.

[github-actions]

Benchmark Results

Benchmark	Main	PR	Change
evaluator/tictactoe	824.98 µs	831.88 µs	+0.8%
evaluator/JMT	47.18 ms	46.94 ms	-0.5%
tictactoe/rust	1.46 s	1.45 s	-0.4%
tictactoe/typescript	1.16 s	1.17 s	+0.1%
tuples/rust	1.63 s	1.64 s	+1.1%
tuples/typescript	1.49 s	1.52 s	+1.9%