Feature: basic pattern matching for data-types

[alexkeizer]

We can attempt to define a data_def command that has the same syntax as regular def, but allows a rudimentary form of defining recursive functions through pattern matching.

We already have Fix.dest which will unfold an element of type (Fix F) \alpha to an element of F (Fix \alpha).
In the framework, F will be the Base type, which is in turn just an application of the inductively defined Shape type, so we should be able to do normal pattern matching on the result of Fix.dest. Our data_def wrapper could use this trick internally.

The challenge is defining a recursive function; I don't expect Lean to be able to recognize this will terminate in finite time. Thus, our wrapper should come up with a decreasing measure, using the decreasing_by machinery.
Combined, that should let us define recursive functions.

A downside is that well-founded recursion generally has worse def-eqs than structural recursion. I'm not a 100% sure where recursion using MvQPF.Fix.rec fits, but presumably we will want a proper equation compiler at some point. This wrapper is a nice stepping stone towards that, though.