-\documentclass{article}
+\documentclass[8pt,twocolumn]{extarticle}
\usepackage[bookmarks=false,ps2pdf]{hyperref}
\usepackage[american]{babel}
\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}