Autoinduct, add more tests

[tlringer]

Some cases to test:

• Function on both sides of equality
• Multiple different fixpoints occur in goal
• Function constant is an alias for another constant, which wraps the fixpoint
• Under binders (ambitious)
• Different numbers of arguments
• Currying
• Let

Probably more.

[tlringer]

Many are done, may add more later to test some of the remaining three cases mentioned here though (let, binders, currying)