Add support for mutually recursive functions in Lean

[sonmarcho]

Mutually recursive functions are currently not supported in Lean, because the syntax for the termination_by, decreasing_by clauses in case of mutually recursive functions is not obvious. Once this is done (or we fix this by allowing extrinsic proofs of termination in a fashion similar to what we do in HOL4 now) we will need to reactivate the compilation of the betree.

[sonmarcho]

I added support for partial functions for the Lean backend (see https://github.com/AeneasVerif/aeneas/tree/main/backends/lean/Base/Diverge) so this no longer is an issue.