intro_clear

#_

Synopsis:

#_

Pre-conditions:

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

Action:

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

New sequents to prove:

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