Induction in the presence of mutually recursive functions

[Bronsa]

Imandra cannot generally synthesize induction schemes for mutually recursive functions, a lot of of the times in the presence of mutually recursive functions, induction would just never work.

Users can provide induction schemes manually (using a custom functional induction scheme), but usually it's much better (if possible) to write in a style that doesn't require mutual recursion (especially in higher order position)