feat: recipe for logical fragments and multiplicative linear logic

[fmontesi]

This PR:

• Adds multiplicative linear logic (MLL) as an example of how a fragment can be derived from a larger inference system (CLL), using Subtype and local recursive functions to eliminate irrelevant cases (see the example in the docstring).
• Puts CLL under the right Cslib.Logic namespace.
• Shortens a few simple definitions for CLL in the expected way.

[thomaskwaring]

This all looks very reasonable to me, it would be nice of course to see some theorems stress-testing the definitions, but that can happen down the track.

One suggestion (for here or in a follow-up) would be to define a custom cases / induction principle for, say, MLL.Proposition — it would package up the process of unpacking the predicate and discharging unreachable cases, and might be a more idiomatic way to set up an API boundary.

[fmontesi]

@thomaskwaring
I think that's a very good idea, I'll experiment with it when I find a moment.

[chenson2018]

A few small style questions. The removal of grind lints seems nice here too.

[chenson2018]

I'm approving but disabling auto-merge, as I think the open scoped I mentioned in my last comment can be removed.