cut sterm

P must be a type.

It closes the current sequent.

It opens two new sequents. The first one has conclusion P → G where G is the old conclusion. The second sequent has conclusion P and hypotheses the hypotheses of the current sequent to prove.