Edit Menu:

Delete Command

You can use the Delete command to delete a given, a variant of a given or goal, a gap in the proof, or a step in the proof. Select whatever you want to delete and give the Delete command (or press the delete key on the keyboard), and if the deletion is allowed, it will be done.

You can delete any given or any variant of a given or goal, and you can select several givens or variants and delete them all in one step. This can be useful if your given list is getting long and you are sure that you won't need certain givens. But you probably shouldn't delete givens unless you are sure that you won't need them.

You cannot delete a gap or a step in the proof if it is needed later in the proof. The last step in a proof or subproof is always needed, because it is what justifies the final conclusion of the proof, so you can never delete the last step in a proof.