This rule can be used forwards to use a s=t (equality) formula to substitute t for s or vice versa in another formula in the proof, or backwards to substitute t for s or vice versa in a goal line to derive a new goal.
To use it forwards:

1. select an empty line and click on Equality Substitution.
2. then select the s = t formula you wish to use in the substitution (this line must be in the scope of the empty line).
3. then select the line you want to substitute the terms in (this line must be in the scope of the empty line).
4. select from the list provided the substitution you wish to perform, by entering the number of the substitution.
5. if there is more then one occurrence of the term you are going to replace in your formula, you will be prompted to enter the formula you are trying to derive from the substitution. If you input no formula here, all occurrences will be substituted by default. If there is only one occurrence of the term to replace, this step is skipped.
6. the formula with the specified terms replaced will be added to your proof.

1. select the goal you wish to replace a term in and click on Equality Substitution.
2. then select the equality formula you wish to use for the substitution.
3. select from the list provided the substitution you wish to perform, by entering the number of the substitution.
4. if there is more then one occurrence of the term you are going to replace in your formula you will be prompted to enter the formula you are trying to derive from the substitution. If you input no formula here, all occurrences will be substituted by default. If there is only one occurrence of the term this step is skipped.
5. the formula with the specified terms replaced will be added as a new goal to your proof.