This rule can only be used backwards from a goal line to prove an intermediate result on the way to the goal (this result is proved in a seperate box).
To use this rule backwards:

1. select the goal line you wish to use for this rule and click on Lemma.
2. when prompted enter the intermediate goal you wish to prove (this formula must only contain relation symbols, function symbols or constants in the signature of the box you are working in).
3. a double box will then be added to your proof with the left hand box containing you intermediate goal as a conclusion and the right hand box containing it as an assumption and the goal you selected as a conclusion - splitting the proof into two parts.