[@@otf] induction hint

[Bronsa]

No description provided.

[Bronsa]

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 :otf-flg (Onward Thru the Fog) allows you to override this chickening out. When :otf-flg is t, the system will push all the initial subgoals and proceed to try to prove each, independently, by induction.