## Edit Menu:

# Insert Command

You can use the Insert command to insert additional steps anywhere in
your proof. Select the gap or step before which you want the
additional steps to appear, and give the Insert command. A dialog box
will open, asking whether there is a goal that you want to achieve with
the additional steps. Your goal can be either to prove a statement or to
define a variable, or you can say that you have no goal. Click OK, and a
new gap will be inserted into the proof, with the goal you specified.

If your goal is to prove a statement, then you might want to set off
the proof as a lemma. If so, click the Lemma check box before clicking
OK. This has the same effect as selecting the gap after it has been
inserted and giving the Lemma command.