+\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}