In this paper, we propose a new lemma facility, called the strong contraction rule, for model elimination calculus, and we study some implementation issues of strong contraction in a PTTP-based theorem prover. Strong contraction has the ability to shorten possible proofs and prevent some irrelevant computation to a target goal. Strong contraction never broadens the search space, in principle, and thus, has a stable effect on the acceleration of top-down proof search. However, it is difficult to embed the strong contraction into a PTTP-based theorem prover, because strong contraction imposes a truncation operation of center chains in model elimination calculus. We show a self-truncation-style Prolog code, which makes it possible to retain the high performance of a PTTP-based prover with strong contraction. Finally, we evaluate the performance and effect of strong contraction by performing some experiments.