Desugaring of `Case`

Currently `Case` desugars to a series of nested `let` expressions, e.g.:
```
exp_of (case x = e of C a b c -> k)
=> let x = exp_of e in
if ... then
let a = proj 0 x; b = proj 1 x; c = proj 2 x in exp_of c
else fail
```
This causes issues when the pattern variables (`a`,`b`,`c`) shadow the `Case` variable (`x`), decoupling the binding structure of compiler expressions from semantic expressions. This requires keeping around invariants on a lack of shadowing in various places where we might otherwise hope to avoid them.

@myreen suggests an alternative desugaring which could help:
```
exp_of (case x = e of C [a,b,c] -> k)
=> let x = exp_of e in if ... then (\ a b c. exp_of c) (proj 0 x) (proj 1 x) (proj 2 x) else fail
```
In this desugaring, `x` can never be shadowed by any of the pattern variables - we would no longer need to carry around the invariants.

An initial approach could be to define an alternative `exp_of` and prove equivalence to the old one. Proofs can then choose which one to use. Better yet is to replace the existing `exp_of` and update all proofs.