This rule can only be applied backwards to a FOR ALL goal line. The rule adds a new box to the proof which declares a skolem constant and has the sub formula inside the forall statement as a conclusion with the skolem constant replacing the outermost for all variable to the in the formula.
To use this rule backwards:

1. select the FOR ALL goal line to use and click on For All Introduction.
2. a new box is then added to the proof which declares a skolem constant (e.g. sk1) and has the FOR ALL formula's sub formula as a new goal with the variable replaced by the skolem constant.