a $\l$-variable $x_{\a}$ of type $\neg A$.

2.  A typed $\l\m$-term $M$ is translated into an $\l$-term $M^{\diamond}$ as follows:

    -   $\{x\}^{\diamond} = x$

    -   $\{\l x. M\}^{\diamond} = \l x. M^{\diamond}$

    -   $\{(M \; N)\}^{\diamond} = (M^{\diamond} \; N^{\diamond})$

    -   $\{\m \a. M\}^{\diamond} = (T_A \;\; \l x_{\a}. M^{\diamond})$ if the type of $\a$ is $\neg A$

    -   $\{(\a \; M)\}^{\diamond} = (x_{\a} \; M^{\diamond})$

<!-- -->

1.  $M^{\diamond}[x :=N^{\diamond}] = \{M[x:=N]\}^{\diamond}$.

2.  $M^{\diamond}[x_{\a} := \l v. (x_{\a} \; (v \; N^{\diamond}))]
     \tr_{\beta}^* \{M[(\a \; L) := (\a \; (L \; N))]\}^{\diamond}$.

By induction on $M$. The first point is immediate. For the second, the only interesting case is $M = (\a \; K)$. Then, $M^{\diamond}[x_{\a} := \l v. (x_{\a} \; (v \; N^{\diamond}))] =(
\l v. (x_{\a} \; (v \; N^{\diamond})) \ K^{\diamond}[x_{\a} := \l
v. (x_{\a} \; (v \; N^{\diamond}))]) $ $\tr_{\b} \ (x_{\a}
\;(K^{\diamond}[x_{\a} := \l v. (x_{\a} \; (v \; N^{\diamond}))]
\; N^{\diamond}) \tr_{\b}^*(x_{\a} \;(\{K[(\a \; L) := (\a \; (L
\; N))]\}^{\diamond} \; N^{\diamond})= \{M[(\a\; L) := (\a \; (L
\; N))]\}^{\diamond}$.

\[simulation1\] Let $M \in {\cal M}'$.

1.  If $M \tr_{\b} N$, then $M^{\diamond} \tr_{\b}^+ N^{\diamond}$.

2.  If $M \tr_{\m} N$, then $M^{\diamond} 