Edit Menu:

Rejustify Command

If you select a step in the proof and give the Rejustify command, then the step and its justification will be deleted, and they will be replaced by a gap whose goal is to prove the assertion.

Note that if the step is justified by a subproof, you can use the Rejustify command even if the subproof still has gaps in it. For example, suppose you are proving a statement of the form P→Q, and you begin by using the Direct command. This would create a subproof in which it is assumed that P is true, and you must prove that Q is true. The subproof would justify the assertion that P→Q is true. While trying to prove Q in the subproof, you might run into trouble and decide that you would have been better off proving P→Q by proving the contrapositive. If so, click on the assertion P→Q, which will select the assertion and the subproof that justifies it, and give the Rejustify command. The assertion and subproof will disappear, and be replaced by a gap whose goal is P→Q. Now you can select the goal and give the Contrapositive command.