The basic command for starting out is the start command, which takes the initial version of the left side of the equation as a parameter. A variant is the startfor command, which has two parameters, the name or format of the theorem to be proved and the initial term.
The getleftside and getrightside commands allow one to get one side of a theorem as the initial term in a new proof session, in which the name/format environment variable will automatically be set to the theorem name or format. The autoedit command creates a proof session identical to that one has obtained when one proves the theorem, and sets the name/format to the name or format of the theorem.
The getenv command allows one to get a proof environment saved by name; saveenv or backupenv (the former takes a name/format as a parameter; the latter uses the current name/format or a default) allow one to save proof environments on the desktop.