Allow more than one initial subgoal to be pushed for induction

The value of this flag is normally

Suppose you submit a conjecture to the theorem prover and the system splits
it up into many subgoals. Any subgoal not proved by other methods is
eventually set aside for an attempted induction proof. But upon setting aside
the second such subgoal, the system chickens out and decides that rather than
prove n>1 subgoals inductively, it will abandon its initial work and
attempt induction on the originally submitted conjecture. The

Even when you don't expect induction to be used or to succeed, setting the

For `defthm` and `thm`, `rule-classes` and `hints`. It may
be supplied as in the following examples; also see defthm.

(thm (my-predicate x y) :rule-classes nil :otf-flg t) (defthm append-assoc (equal (append (append x y) z) (append x (append y z))) :hints (("Goal" :induct t)) :otf-flg t)

The `defun` via the `xargs`
declare option. When you supply an