If SELECT is invoked on any sequent of a proof but the main goal, a read-only term window onto that subgoal is generated. This is useful, for example, if one wants to use a term from a sequent as an argument to a tactic, and one doesn't want to have to retype in the term.