Auto-including well-foundedness functions and axioms when they are used

[marcoeilers]

This is an extension of the termination plugin that auto-includes the relevant functions and axioms used by the generated proof obligations if the program does not already include them. This is to address the problem that writing decreases e without having the relevant input currently leads to a rather cryptic error message that informs the user that the functions "bounded" and "decreasing" were not found in the program, without any hint that an import is missing (and what the imported file should be).

That is,

• it collects all decreases clauses in the program
• for a decreases term of type T, it checks if the domain TWellFoundedOrder is already in the program
• if not, it adds it to the program (by generating a second program containing only the relevant input and adding it to the program being verified)

For programs that contain all relevant definitions, nothing changes. For programs that already contain some but not all required imports, only the missing ones are added.

Instead of adding new tests, this PR removes (some of) the existing imports for some termination tests.

[marcoeilers]

I'm not sure who to ask to review this. Who's worked on the termination plugin before? @ArquintL maybe?