This rule can be used forwards to derive the right sub formula of a FOR ALL IMPLIES formula using a formula which matches the left subformula with a term substituted for the FOR ALL variable, or backwards to derive the left sub formula of a FOR ALL IMPLIES formula using a formula which is the right subformula with a term substituted for the FOR ALL variable.
To use it forwards:

1. select an empty line and click on For All Arrow Elimination.
2. then select the FOR ALL ARROW formula you wish to eliminate from (this line must be in the scope of the empty line).
3. then select a formula which matches the left sub formula of the FOR ALL ARROW formula with its FOR ALL variable substituted for a term (this line must also be in the scope of the empty line).
4. the right sub formula will then be added as a new line to your proof with any occurrences of the FOR ALL variable substituted for the term which mapped to them in the formula used to eliminate the IMPLIES.

1. select a goal line corresponding to the right sub formula of a FOR ALL ARROW formula you wish to eliminate and click on For All Arrow Elimination.
2. then select the FOR ALL ARROW formula you wish to eliminate from (this line must be in the scope of the goal line).
3. the left sub formula will then be added as a new goal line to your proof with any occurrences of the FOR ALL variable substituted for the term which mapped to it in the formula used to eliminate the FOR ALL ARROW formula.