Extend `iInduction` with support for induction schemes containing `Forall`.

This instance is based on an instance for Simuliris. We also generate a proper error message if an IntoIH instance is missing.

This MR also contains tests for both.

This MR closes issue #430 (closed).