intro H
intro [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 if provided; otherwise it is automatically generated.