Lemma 2.1.4.
Assuming that:
M
and
N
are
λ
-terms
Then
(1)
FV
(
M
∗
)
⊆
FV
(
M
)
;
(2)
M
↠
β
M
∗
;
(3)
If
M
→
β
N
, then
N
↠
β
M
∗
.