#id

The conclusion of the sequent to prove must be an implication or a universal quantification.

It applies the right introduction rule for implication, closing the current sequent.

It opens a new sequent to prove adding to the hypothesis the antecedent of the implication and setting the conclusion to the consequent of the implicaiton. The name of the new hypothesis is H.