Induction improvements

[mezpusz]

This PR includes various improvements and features on (mostly) inductive reasoning:

• Function definitions from define-fun[-rec] blocks in SMTLIB are handled specially for inductive reasoning via some new options, including using them as rewrite rules (-fnrw on) and creating induction schemas based on their case distinctions/well-founded orders (-sik recursion).
• Added two new induction schedules and changed the structural induction schedule to a new one.
• Fixed a couple of bugs which came out from combining previously untested combinations of induction and other options.
• Added parsing for define-funs-rec (exists in SMTLIB 2.6), allowing for mutually recursive functions.

While creating the above mentioned schedules, the features were extensively tested, so hopefully everything works at least as well as they worked before.

[quickbeam123]

This also contains two new induction schedules: struct_induction_tip and intind_oeis optimized for the tip benchmarks Tons of Inductive Problems and for OEIS problems (https://easychair.org/publications/paper/3hgH).

[mezpusz]

could you please add comments explaining what the new functions do and what they're used for (when it's not obvious from the name)?

@hzzv I added comments where I saw fit (including stuff in Induction.*pp which was not commented before). Feel free to add something that you feel should be documented (better).