cut

cut P as H

Synopsis:

cut sterm [as id]

Pre-conditions:

P must have type Prop.

Action:

It closes the current sequent.

New sequents to prove:

It opens two new sequents. The first one has an extra hypothesis H:P. If H is omitted, the name of the hypothesis is automatically generated. The second sequent has conclusion P and hypotheses the hypotheses of the current sequent to prove.