Miscellaneous fixes to formal overview document.

[ioannad]

In particular:

• In previous reviews we dropped the kind property of labels, and went for labels of the form catch^? [t*] after all.
• Changed some ^n to * where appropriate.
• Removed occurrences of "we ..." formulations.

[aheejin]

When do we use n and when do we use *? I might have asked this before but I'm still confused.

And while this LGTM, I don't think we need to be very strict about styles in this markdown doc :)

[ioannad]

@aheejin

When do we use n and when do we use *? I might have asked this before but I'm still confused.

AFAIU we use n when it's relevant to other parts of the rule, meaning that n appears in two or more unrelated operations of the rule. For example, if the rule has a val^n and a label_n{}. (Can't think of another example atm, I hope this clarifies this a bit!)