Theorem 2.1.8. Assuming that:

$M$ $β$ -reduces to $N$ in $n$ steps

Then

N ↠_{β} M^{n *}

.