Matita HomeMatita Homecut P as H
P must have type Prop.
It closes the current sequent.
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.