+\item $ex\_intro$.
+ We must prove that
+ $$\lambda x:\N.\lambda f:\sem{P}.<x,f> \R \forall x.(P\to\exists x.P(x)$$
+ that leads to prove that foreach n
+ $\underline{ex\_into}~n \R (P\to\exists x.P(x))[\underline{n}/x]$.\\
+ Evaluating the substitution we have
+ $\underline{ex\_into}~n \R (P[\underline{n}/x]\to\exists x.P(x))$.\\
+ Again by definition of $\R$ we have to prove that given a
+ $m \R P[\underline{n}/x]$ then $\underline{ex\_into}~n~m \R \exists x.P(x)$.
+ Expanding the definition of $\underline{ex\_intro}$ we have
+ $<n,m> \R \exists x.P(x)$ that is true since $m \R P[\underline{n}/x]$.
+