Formatting STS rules

The formatting of `let` seems weird to me and inconsistent across the document; I would suggest the following two versions to be applied uniformly and consistently:
1. for very small binding, just keep it in the same line as the rule/constructor, e.g.
```agda
RULE: let x = 5 in ...
...
```
2. for longer cases, **always** use the following format:
```agda
RULE:
let
BINDING #1
BINDING #2
...
BINDING #k
in
...
```
(if you cannot spare the two spaces caused by the suggested indentation, the problem lies elsewhere..)

---

While I'm at it, I saw some occurrences of the function arrow for rule hypotheses, which should be uniformly replaced with `∙` in my opinion and formatted the same way as `LEDGER` currently is, i.e.
```agda
RULE : let ... in
∙ HYPOTHESIS #1
∙ HYPOTHESIS #2

∙ HYPOTHESIS #n
────────────────────────────────
CONCLUSION
```
(notice how the 'dots' lie outside and hypothesis, horizontal rule and conclusion are all lined up.

_Originally posted by @omelkonian in https://github.com/IntersectMBO/formal-ledger-specifications/pull/336#discussion_r1430365405_