We want to step into the consequent of this formula.
Apply the StepintoSubFormula tactic
Start the subformula selection mode(press ctrl+F10) to select the subformula.
Select the consequent of the implication.
Enter the subformula id.
Apply the tactic.
A new formula node is generated in the synthesis tree.
The consequent becomes the active formula whereas the antecedent is added in the frame context.