This commits enable the possibility to use variants
with different types/well-founded relations for
mutually recursive functions. This is useful if the
termination of sub-groups of those functions requires
a finer termination argument.

Example use case:
Suppose for example the following mutually recursive
function structure:

type t = A (list t)
let rec f (x:t) (...other args...)
  variant { x , other variants }
= ... f x (...different args...)...
with g (l:list t) (...other args...)
  variant { l }
= ...

The global termination argument is structural descent
trough the type t. However, as it is not enough for f
which perform a non-structural recursive calls, we add
other variants. Such variants were forbidden under the
previous behavior because f and g variants were
considered incompatible: As x and l have different
types, it was impossible to write the lexicographic
comparison of both n-uplets (even when completing g's
list).

The new behavior for mutual recursive calls is the
following: We first scan both variants to find the
longest compatible common prefix, e.g prefixes for
which types and relations are the same. Additionally,
we allow the last elements of such prefix to have
different types if their well-founded relation is
structural descent. Then, we generate a lexicographic
descent obligation on those prefixes only.

We still enforce that in a mutually recursive group,
the first component of each variant must corresponds
to the same well-founded relation. This event is much
more likely to be symptomatic of an error, as functions
with such fully mismatched variants cannot call each
other anyway. Moreover, one can always break them in
different recursive groups.