intros intros-spec

If hyps specifies a number of hypotheses to introduce, then the conclusion of the current sequent must be formed by at least that number of imbricated implications or universal quantifications.

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

It opens a new sequent to prove adding a number of new hypotheses equal to the number of new hypotheses requested. If the user does not request a precise number of new hypotheses, it adds as many hypotheses as possible. The name of each new hypothesis is either popped from the user provided list of names, or it is automatically generated when the list is (or becomes) empty.