Formatting STS rules

[WhatisRT]

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.

RULE: let x = 5 in ...
  ...

2. for longer cases, always use the following format:

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.

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 #336 (comment)