suppose term ( id )

The conclusion of the sequent to prove must be an implication.

It applies the right introduction rule for the implication, closing the current sequent (in Natural Deduction this corresponds to the introduction rule for the implication).

It opens a new sequent to prove the consequent of the implication adding the antecedent A to the hypotheses. The name of the new hypothesis is H.