Local `match` and `record` expression

We can have a local match and record expression by lifting these to synthesized global definitions. However, we loose definitional equalities by doing so. But most of the time this should not be relevant to the user, assuming that we often have to match on simple products such as tuples.