exact p
exact sterm
The type of p must be convertible with the conclusion of the current sequent.
It closes the current sequent using p.
None.