feat: structural mutual recursion (#4575)

This adds support for mutual structural recursive functions.

For now this is opt-in: The functions must have a `termination_by
structural …` annotation (new since #4542) for this to work:

```lean
mutual
inductive A
  | self : A → A
  | other : B → A
  | empty
inductive B
  | self : B → B
  | other : A → B
  | empty
end

mutual
def A.size : A → Nat
  | .self a => a.size + 1
  | .other b => b.size + 1
  | .empty => 0
termination_by structural x => x
def B.size : B → Nat
  | .self b => b.size + 1
  | .other a => a.size + 1
  | .empty => 0
termination_by structural x => x
end
```

The recursive functions don’t have to be in a one-to-one relation to a
set of mutually recursive inductive data types. It is possible to ignore
some of the types:

```lean
def A.self_size : A → Nat
  | .self a => a.self_size + 1
  | .other _ => 0
  | .empty => 0
termination_by structural x => x
```

or have more than one function per argument type:

```lean
  def isEven : Nat → Prop
    | 0 => True
    | n+1 => ¬ isOdd n
  termination_by structural x => x

  def isOdd : Nat → Prop
    | 0 => False
    | n+1 => ¬ isEven n
  termination_by structural x => x
```


This does not include

 * Support for nested inductive data types or nested recursion
* Inferring mutual structural recursion in the absence of
`termination_by`.
 * Functional induction principles for these.
* Mutually recursive functions that live in different universes. This
may be possible,
maybe after beefing up the `.below` and `.brecOn` functions; we can look
into this some
   other time, maybe when there are concrete use cases.

---------

Co-authored-by: Richard Kiss <him@richardkiss.com>
Co-authored-by: Tobias Grosser <tobias@grosser.es>