Tick
   
 

This rule can be used forwards to copy a previous line in the proof (this is done to increase readability) or backwards to complete a box or proof by matching the goal line with an identical line shown in the proof.
To use it forwards:

  1. select an empty line and click on Tick.
  2. then select the line you wish to copy (this line must be in the scope of the empty line).
  3. a new line containing the same formula as line you selected will then be added to the proof.
To use it backwards:
  1. select the goal you wish to apply tick to and click on Tick.
  2. then select the line which matches the goal formula you selected (this line must be in the scope of the goal line).
  3. the box containing the goal line will then close (the empty line is removed and the box will turn grey).