This rule can be used forwards to add the line t=t, where t is a closed term in the signature, to your proof or backwards to justify a t=t goal line by the reflexivity law.
To use it forwards:

1. select an empty line and click on Reflex.
2. when prompted enter a closed term which is in the signature of the box you are working in .
3. the formula t=t, where t is the term you entered, will then be added to your proof.

1. select the t=t goal line, where t is a term, you wish to justify and click on Reflex.
2. the goal line will then be justified closing the box it is in (the empty line is removed and the box will turn grey).