This paper describes a mechanism to generalize mathematical results in type theory based proof assistants. The proposed mechanism
starts from a proved theorem or a proved set of theorems (a theory) and makes it possible to get less specific results that
can be instantiated and reused in other contexts.
This work was done during a postdoctoral appointment at Universidade do Minho (Portugal). It was supported by the Portuguese
Science Foundation (Fundação para a Ciencia e a Technologia) under the Fellowship PRAXIS-XXI/BPD/22108/99.