The type of p must be convertible with the conclusion of the current sequent.

It closes the current sequent using p.

None.