Specify Proof Tactic

      If the user has selected Specify induction tactics? in the menu Specify Proof Directives?, a menu Specify Proof Tactic appears, with a list of all the conjectures in the current batch. Next to each conjecture is a number of options. Select one of the following:

None

Select this if induction is not to be used to prove the conjecture.

Ind

A number of items will be proposed offering a choice of induction variables (what to do induction on) and constructor sets. Choose one.