One of the key features of the logical environment is automation. One way in which this gets exhibited in is in inheritance of results. As we described, type theories are typically constructed by refinement. For instance, the classical Nuprl theory is the constructive theory refined with the axiom of choice. Mathematically, the constructive results are valid in the classical theory, and automates that task of importing all the theorems and proof tools to the classical subtheory.
The same mechanism is used to transfer results between theories. Once the relation is justified (or asserted) between Nuprl and HOL, the results from HOL, including the theorems and proof tools are made available in Nuprl.