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 PQ, 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 PQ 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 PQ by proving the contrapositive. If so, click on the assertion PQ, 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 PQ. Now you can select the goal and give the Contrapositive command.