Lemma 2.1.5.
Takahashi translation
preserves
β
-contraction:
(
(
λ
x
.
P
)
Q
)
∗
↠
β
(
P
[
x
:
=
Q
]
)
∗
.