few more cases

diff --git a/helm/papers/system_T/t.tex b/helm/papers/system_T/t.tex
index fc6b1bd1e66a382736cb9542a84ae0737640c938..1e1b6c46c30ab488598a54077be525408591878b 100644 (file)
--- a/helm/papers/system_T/t.tex
+++ b/helm/papers/system_T/t.tex
@@ -156,6 +156,18 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$.
   and $snd$ we obtain $f~n_p~g_p$ that we know is in relation $\R$ with $Q$
   since $g_p \R P[\underline{n_p}/x]$.
 
+\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]$.
+
 \item $false\_ind$. 
   We have to prove that $\bot_{\sem{Q}} \R \bot \to Q$. 
   Trivial, since there is no $m \R \bot$.
@@ -164,6 +176,14 @@ We proceed to prove that all axioms $ax:Ax$ are realized by $\sem{ax}$.
   Since there is no $n$ such that $0 = S n$ is true... \\
   $\underline{discriminate}~n \R 0 = S~\underline{n} \to \bot$ for each n.
 
+\item $injS$.
+  We have to prove that for each $n_1$ and $n_2$\\
+  $\lambda \_:\N. \lambda \_:\N.\lambda \_:1.*~n_1~n_2 \R 
+  (S(x)=S(y)\to x=y)[n_1/x][n_2/y]$.\\
+  Assuming $m \R S(n_1)=S(n_2)$ we have to prove
+
+  
+
 \end{itemize}
 
 \begin{thebibliography}{}