This rule can backwards only to eliminate a THERE EXISTS formula, creating a new box and a new name replacing the exists variable, to prove a goal.
To use it backwards:

1. select the goal line you want to prove using the rule and click on There Exists Elimination.
2. then select the THERE EXISTS formula you wish to eliminate to prove this goal (this line must be in the scope of the goal line).
3. a new box will then be added to your proof declaring a skolem term and assuming the sub formula of the THERE EXISTS formula with the skolem term replacing the THERE EXISTS variable. The conclusion of the box is set the goal formula you selected.