@ sterm

t must have type T₁ → … → T_n → G where G can be unified with the conclusion of the current sequent.

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

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