+
+\noindent
+{\bf example}\\
+Let us prove the following principle of well founded induction:
+\[(\forall m.(\forall p. p < m \to P~p) \to P~m) \to \forall n.P~n\]
+In the following proof we shall make use of proof-terms, since we finally
+wish to extract the computational content; we leave to reader the easy
+check that the proof object describes the usual and natural proof
+of the statement.
+
+We assume to have already proved the following lemmas (having trivial
+realizers):\\
+\[L : \forall p, q.p < q \to q \le 0 \to \bot\]
+\[M : \forall p,q,n.p < q \to q \le (S n) \to p \le n \]
+Let us assume $h : \forall m.(\forall p. p < m \to P~p) \to P~m$.
+We prove by induction on $n$ that $\forall q. q \le n \to P~q$.
+For $n=0$, we get a proof of $P ~q$ by
+\begin{eqnarray}
+B & \equiv & \lambda q.\lambda h_0:q \le 0. h ~q~ \nonumber\\
+& & \quad (\lambda p.\lambda k:p < q. false\_ind ~(L~p~q~k~h_0)) \nonumber
+\end{eqnarray}
+In the inductive case, we must prove that, for any $n$,
+\[(\forall q. q \le n \to P~q) \to (\forall q. q \le S n \to P~q)\]
+Assume $h_1: \forall q. q \le n \to P q$ and
+$h_2: q \le S ~n$. Let us prove $\forall p. p < q \to P~p$.
+If $h_3: p < q$ then $(M~ p~ q~ n~ h_3~ h_2): p \le n$, hence
+$h_1 ~p ~ (M~ p~ q~ n~ h_3~ h_2): P~p$.\\
+In conclusion, the proof of the
+inductive case is
+\begin{eqnarray}
+I & \equiv & \lambda n.\lambda h_1:\forall q. q \le n \to P~ q.\lambda q.\lambda h_2:q \le S n. \nonumber\\
+ & & \quad h ~ q ~ (\lambda p.\lambda h_3:p < q.h_1 ~p~ (M~ p~ q~ n~ h_3~ h_2))
+ \nonumber
+\end{eqnarray}
+(where $h$ is free in I).
+The full proof is
+\begin{eqnarray}
+& \lambda h:\forall m.(\forall p. p < m\to P~p)\to P~m.\lambda m. &\nonumber\\
+& \quad nat\_ind ~B ~ I ~m~m~ (le\_n ~ m) & \nonumber
+\end{eqnarray}
+
+where $le\_n$ is a proof that $\forall n. n \le n$, and the free $P$ in the definition of $nat_{ind}$ is instantiated with $\forall m.m \le m \to P~m$.\\
+Form the previous proof,after stripping terminal objects,
+and a bit of eta-contraction to make
+the term more readable, we extract the following term (types are omitted):
+
+\[R' \equiv \lambda f.\lambda m.
+R~ (\lambda n.f ~n~ (\lambda q.*))~
+(\lambda n\lambda g\lambda q.f ~q~g)~m ~m\]
+
+The intuition of this operator is the following: supose to
+have a recursive definition $h q = F[h]$ where $q:\N$ and
+$F[h]: A$. This defines a functional
+$f: \lambda q.\lambda g.F[g]: N\to(N\to A) \to A$, such that
+(morally) $h$ is the fixpoint of $f$. For instance,
+in the case of the fibonacci function, $f$ is
+\begin{eqnarray}
+fibo & \equiv & \lambda q. \lambda g. if~ q = 0~then~ 1~ else \nonumber\\
+& & \quad if~ q = 1~ then~ 1~ else ~ g (q-1)+g (q-2) \nonumber
+\end{eqnarray}
+
+So $f$ build a new
+approximation of $h$ from the previous approximation $h$ taken
+as input. $R'$ precisely computes the mth-approximation starting
+from a dummy function $(\lambda q.*_A)$. Alternatively,
+you may look at $g$ as the ``history'' (curse of values) of $h$
+for all values less or equal to $q$; then $f$ extend $g$ to
+$q+1$.
+
+Let's compute for example
+\begin{eqnarray}
+R'~fibo~2 & \leadsto &
+ R~ (\lambda n.fibo ~n~ (\lambda q.*))~
+ (\lambda n\lambda g\lambda q.fibo ~q~g)~2 ~2\nonumber\\
+& \leadsto &
+ (\lambda n\lambda g\lambda q.fibo ~q~g)~1~
+ (R~
+ (\lambda n.fibo ~n~ (\lambda q.*))~
+ (\lambda n\lambda g\lambda q.fibo ~q~g)~1)~
+ 2 \nonumber\\
+& \leadsto &
+ \lambda q.fibo ~q~
+ (R~
+ (\lambda n.fibo ~n~ (\lambda q.*))~
+ (\lambda n\lambda g\lambda q.fibo ~q~g)~1)~
+ 2 \nonumber\\
+& \leadsto &
+ \lambda q.fibo ~q~
+ ((\lambda n\lambda g\lambda q.fibo ~q~g)~0~
+ (R~
+ (\lambda n.fibo ~n~ (\lambda q.*))~
+ (\lambda n\lambda g\lambda q.fibo ~q~g)~0))~
+ 2 \nonumber\\
+& \leadsto &
+ \lambda q.fibo ~q~
+ (\lambda q.fibo ~q~
+ (R~
+ (\lambda n.fibo ~n~ (\lambda q.*))~
+ (\lambda n\lambda g\lambda q.fibo ~q~g)~0)
+ )2 \nonumber\\
+& \leadsto &
+ \lambda q.fibo ~q~
+ (\lambda q.fibo ~q~
+ (\lambda n.fibo ~n~ (\lambda q.*)))2
+ \nonumber\\
+& \leadsto &
+ fibo~2~(\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) \nonumber\\
+& \leadsto &
+ (\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) 1 +
+ (\lambda q.fibo ~q~ (\lambda n.fibo ~n~ (\lambda q.*))) 0 \nonumber\\
+& \leadsto &
+ fibo ~1~ (\lambda n.fibo ~n~ (\lambda q.*)) +
+ fibo ~0~ (\lambda n.fibo ~n~ (\lambda q.*)) \nonumber\\
+& \leadsto &
+ 1 + 1 \nonumber
+\end{eqnarray}
+Note that the second argument of $fibo$ is always a method to calculate all the prvious values of $fibo$. DA CAPIRE (per me) come mai $\lambda n$ non viene usata...
+CAPITA CON csc:
+
+n non serve perche' c'e' una relazione logica di n con q,
+in particolare $q <= Sn$ ... quindi $q < n$ (lemma M)...
+e quindi posso usare come history $< n$ una history $< q$.
+il $\lambda h2$ essendo $[[q <= Sn]]$ = 1 viene scartata.
+
+se si spiega come array viene decente... forse. lunedi' provo a scrivere
+meglio.
+
+\Section{Inductive types}