Improved mutual induction

[Vtec234]

Many of the proofs in Syntax.* are by mutual induction, but our mutual_induction tactic does not support any convenience features. The task is to simplify these proof scripts, either by improving the tactic, writing a new one, or using https://github.com/ionathanch/MutualInduction assuming it supports the necessary features.

The ideal tactic might support (see also here and Zulip):

• Automatic abstraction and reverting of non-variable indices.
• generalize syntax
• Multiple goals rather than one big conjunctive goal.
• Declaring multiple theorems at once in a mutual block, rather than as consequences of one big theorem.

The Lean language reference on mutual inductive types is here.