\begin{document}
-\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.type.tex}
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_beta.type}
\bigskip
-\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.body.tex}
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_comp.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_delta.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_refl.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_tau.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_upsilon.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0.pr0_zeta.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.type}
+
+\bigskip
+
+\input{matita.lambdadelta.basic_1.pr0.defs.pr0_ind.pr0_ind.body}
\bigskip
\input{matita.lambdadelta.basic_1.pr0.pr0.pr0_confluence.body}
+\bigskip
+
+\ObjRef{pr0}
\ObjRef{pr0_ind}
\ObjRef{pr0_confluence}