lapply sterm

None.

It generalizes the conclusion of the current goal adding as a premise the type of t, closing the current goal.

The new sequent has conclusion T → G where T is the type of t and G the old conclusion.