Olivier Pons: Generalization in Type Theory Based Proof Assistants. TYPES 2000: 217-232