#_

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

It applies the ``a fortiori'' rule for implication, closing the current sequent.

It opens a new sequent whose conclusion is the conclusion of the implication of the original sequent.