Models and termination of proof reduction in the $\\lambda$$\\Pi$-calculus\n modulo theory

We define a notion of model for the $\\lambda$$\\Pi$-calculus modulo theory and\nprove a soundness theorem. We then define a notion of super-consistency and\nprove that proof reduction terminates in the $\\lambda$$\\Pi$-calculus modulo any\nsuper-consistent theory. We prove this way the termination of proof reduction\nin several theories including Simple type theory and the Calculus of\nconstructions .\n