absurd sterm

P must have type Prop.

It closes the current sequent by eliminating an absurd term.

It opens two new sequents of conclusion P and ¬P.