apply

@t

Synopsis:

@ sterm

Pre-conditions:

t must have type T1 → … → Tn → G where G can be unified with the conclusion of the current sequent.

Action:

It closes the current sequent by applying t to n implicit arguments (that become new sequents).

New sequents to prove:

It opens a new sequent for each premise Ti that is not instantiated by unification. Ti is the conclusion of the i-th new sequent to prove.