intro

intro H

Synopsis:

intro [id]

Pre-conditions:

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

Action:

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

New sequents to prove:

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.