This rule can only be used backwards on a not goal line by opening a box which assumes the opposite of the goal line and has a conclusion of bottom.
To use it backwards:
select the goal line, which must be a NOT formula, and click on Not Introduction.
this will add a new box to your proof with the assumption the converse of the goal line and the conclusion bottom.
