CREATE-SUBPROOF : MEXPRCREATE-SUBPROOF is a top-level command.
Creates a new proof in memory from the given lines,
plus all the lines on which they depend, and makes that
the current proof.
The command format for CREATE-SUBPROOF is:
<n>CREATE-SUBPROOF LINES SUBNAME
The arguments have the following meaning:
LINES : List of line ranges to use
SUBNAME : Name for new subproof
TPS documentation homepage