From f654fd9873d09435f10c91554e5b94bd44fd5850 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 8 Sep 2015 13:40:09 +0000 Subject: [PATCH] refactoring meta files for procedural reconstruction of \lambda\delta version 1 --- .../contribs/{LAMBDA-TYPES => procedural/lambdadelta}/Makefile | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/A/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/C/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/C/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/G/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/T/dec.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/T/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/T/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/aplus/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/aplus/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/app/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/aprem/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/aprem/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/aprem/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/arity/aprem.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/arity/cimp.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/arity/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/arity/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/arity/lift1.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/arity/pr3.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/arity/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/arity/subst0.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/asucc/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/asucc/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/cimp/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/cimp/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/clear/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/clear/drop.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/clear/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/clear/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/clen/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/clen/getl.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/cnt/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/cnt/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csuba/arity.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csuba/clear.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csuba/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csuba/drop.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csuba/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csuba/getl.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csuba/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubc/arity.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubc/clear.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubc/csuba.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubc/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubc/drop.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubc/drop1.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubc/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubc/getl.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubc/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubst0/clear.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubst0/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubst0/drop.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubst0/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubst0/getl.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubst0/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubst1/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubst1/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubst1/getl.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubst1/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubt/clear.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubt/csuba.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubt/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubt/drop.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubt/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubt/getl.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubt/pc3.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubt/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubt/ty3.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubv/clear.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubv/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubv/drop.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubv/getl.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/csubv/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/drop/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/drop/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/drop/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/drop1/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/drop1/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/drop1/getl.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/drop1/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/ex0/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/ex0/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/ex1/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/ex1/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/ex2/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/ex2/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/flt/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/flt/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/fsubst0/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/fsubst0/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/getl/clear.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/getl/dec.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/getl/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/getl/drop.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/getl/flt.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/getl/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/getl/getl.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/getl/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/iso/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/iso/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/iso/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/leq/asucc.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/leq/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/leq/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/leq/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/lift/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/lift/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/lift/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/lift/tlt.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/lift1/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/lift1/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/lift1/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/llt/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/llt/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/next_plus/defs.mma | 0 .../lambdadelta/basic_1}/next_plus/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/nf2/arity.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/nf2/dec.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/nf2/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/nf2/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/nf2/iso.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/nf2/lift1.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/nf2/pr3.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/nf2/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pc1/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pc1/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pc3/dec.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pc3/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pc3/fsubst0.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pc3/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pc3/left.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pc3/nf2.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pc3/pc1.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pc3/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pc3/subst1.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pc3/wcpr0.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr0/dec.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr0/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr0/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr0/pr0.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr0/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr0/subst1.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr1/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr1/pr1.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr1/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr2/clen.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr2/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr2/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr2/pr2.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr2/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr2/subst1.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr3/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr3/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr3/iso.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr3/pr1.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr3/pr3.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr3/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr3/subst1.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/pr3/wcpr0.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/preamble.ma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/r/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/r/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/s/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/s/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/sc3/arity.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/sc3/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/sc3/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/sn3/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/sn3/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/sn3/lift1.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/sn3/nf2.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/sn3/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/sty0/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/sty0/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/sty0/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/sty1/cnt.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/sty1/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/sty1/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/subst/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/subst/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/subst/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/subst0/dec.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/subst0/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/subst0/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/subst0/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/subst0/subst0.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/subst0/tlt.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/subst1/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/subst1/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/subst1/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/subst1/subst1.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/theory.ma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/tlist/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/tlist/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/tlt/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/tlt/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/ty3/arity.mma | 0 .../lambdadelta/basic_1}/ty3/arity_props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/ty3/dec.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/ty3/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/ty3/fsubst0.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/ty3/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/ty3/fwd_nf2.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/ty3/nf2.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/ty3/pr3.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/ty3/pr3_props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/ty3/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/ty3/sty0.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/ty3/subst1.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/wcpr0/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/wcpr0/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/wcpr0/getl.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/wf3/clear.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/wf3/defs.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/wf3/fwd.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/wf3/getl.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/wf3/props.mma | 0 .../Basic-2 => procedural/lambdadelta/basic_1}/wf3/ty3.mma | 0 .../contribs/{LAMBDA-TYPES => procedural/lambdadelta}/depends | 0 .../Ground-2 => procedural/lambdadelta/ground_1}/blt/defs.mma | 0 .../Ground-2 => procedural/lambdadelta/ground_1}/blt/props.mma | 0 .../Ground-2 => procedural/lambdadelta/ground_1}/ext/arith.mma | 0 .../Ground-2 => procedural/lambdadelta/ground_1}/ext/tactics.mma | 0 .../Ground-2 => procedural/lambdadelta/ground_1}/plist/defs.mma | 0 .../Ground-2 => procedural/lambdadelta/ground_1}/plist/props.mma | 0 .../Ground-2 => procedural/lambdadelta/ground_1}/preamble.ma | 0 .../Ground-2 => procedural/lambdadelta/ground_1}/theory.ma | 0 .../Ground-2 => procedural/lambdadelta/ground_1}/types/defs.mma | 0 .../Ground-2 => procedural/lambdadelta/ground_1}/types/props.mma | 0 .../Legacy-2 => procedural/lambdadelta/legacy_1}/coq/defs.mma | 0 .../Legacy-2 => procedural/lambdadelta/legacy_1}/coq/props.mma | 0 .../Legacy-2 => procedural/lambdadelta/legacy_1}/preamble.ma | 0 .../Legacy-2 => procedural/lambdadelta/legacy_1}/theory.ma | 0 .../matita/contribs/{LAMBDA-TYPES => procedural/lambdadelta}/root | 0 235 files changed, 0 insertions(+), 0 deletions(-) rename matita/matita/contribs/{LAMBDA-TYPES => procedural/lambdadelta}/Makefile (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/A/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/C/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/C/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/G/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/T/dec.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/T/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/T/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/aplus/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/aplus/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/app/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/aprem/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/aprem/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/aprem/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/arity/aprem.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/arity/cimp.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/arity/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/arity/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/arity/lift1.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/arity/pr3.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/arity/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/arity/subst0.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/asucc/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/asucc/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/cimp/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/cimp/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/clear/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/clear/drop.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/clear/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/clear/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/clen/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/clen/getl.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/cnt/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/cnt/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csuba/arity.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csuba/clear.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csuba/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csuba/drop.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csuba/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csuba/getl.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csuba/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubc/arity.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubc/clear.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubc/csuba.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubc/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubc/drop.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubc/drop1.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubc/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubc/getl.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubc/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubst0/clear.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubst0/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubst0/drop.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubst0/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubst0/getl.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubst0/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubst1/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubst1/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubst1/getl.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubst1/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubt/clear.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubt/csuba.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubt/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubt/drop.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubt/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubt/getl.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubt/pc3.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubt/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubt/ty3.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubv/clear.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubv/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubv/drop.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubv/getl.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/csubv/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/drop/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/drop/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/drop/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/drop1/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/drop1/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/drop1/getl.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/drop1/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/ex0/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/ex0/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/ex1/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/ex1/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/ex2/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/ex2/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/flt/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/flt/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/fsubst0/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/fsubst0/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/getl/clear.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/getl/dec.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/getl/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/getl/drop.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/getl/flt.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/getl/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/getl/getl.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/getl/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/iso/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/iso/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/iso/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/leq/asucc.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/leq/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/leq/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/leq/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/lift/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/lift/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/lift/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/lift/tlt.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/lift1/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/lift1/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/lift1/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/llt/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/llt/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/next_plus/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/next_plus/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/nf2/arity.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/nf2/dec.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/nf2/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/nf2/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/nf2/iso.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/nf2/lift1.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/nf2/pr3.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/nf2/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pc1/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pc1/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pc3/dec.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pc3/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pc3/fsubst0.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pc3/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pc3/left.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pc3/nf2.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pc3/pc1.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pc3/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pc3/subst1.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pc3/wcpr0.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr0/dec.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr0/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr0/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr0/pr0.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr0/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr0/subst1.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr1/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr1/pr1.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr1/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr2/clen.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr2/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr2/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr2/pr2.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr2/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr2/subst1.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr3/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr3/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr3/iso.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr3/pr1.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr3/pr3.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr3/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr3/subst1.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/pr3/wcpr0.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/preamble.ma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/r/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/r/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/s/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/s/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/sc3/arity.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/sc3/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/sc3/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/sn3/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/sn3/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/sn3/lift1.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/sn3/nf2.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/sn3/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/sty0/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/sty0/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/sty0/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/sty1/cnt.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/sty1/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/sty1/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/subst/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/subst/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/subst/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/subst0/dec.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/subst0/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/subst0/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/subst0/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/subst0/subst0.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/subst0/tlt.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/subst1/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/subst1/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/subst1/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/subst1/subst1.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/theory.ma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/tlist/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/tlist/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/tlt/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/tlt/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/ty3/arity.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/ty3/arity_props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/ty3/dec.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/ty3/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/ty3/fsubst0.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/ty3/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/ty3/fwd_nf2.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/ty3/nf2.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/ty3/pr3.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/ty3/pr3_props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/ty3/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/ty3/sty0.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/ty3/subst1.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/wcpr0/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/wcpr0/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/wcpr0/getl.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/wf3/clear.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/wf3/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/wf3/fwd.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/wf3/getl.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/wf3/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Basic-2 => procedural/lambdadelta/basic_1}/wf3/ty3.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES => procedural/lambdadelta}/depends (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Ground-2 => procedural/lambdadelta/ground_1}/blt/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Ground-2 => procedural/lambdadelta/ground_1}/blt/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Ground-2 => procedural/lambdadelta/ground_1}/ext/arith.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Ground-2 => procedural/lambdadelta/ground_1}/ext/tactics.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Ground-2 => procedural/lambdadelta/ground_1}/plist/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Ground-2 => procedural/lambdadelta/ground_1}/plist/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Ground-2 => procedural/lambdadelta/ground_1}/preamble.ma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Ground-2 => procedural/lambdadelta/ground_1}/theory.ma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Ground-2 => procedural/lambdadelta/ground_1}/types/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Ground-2 => procedural/lambdadelta/ground_1}/types/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Legacy-2 => procedural/lambdadelta/legacy_1}/coq/defs.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Legacy-2 => procedural/lambdadelta/legacy_1}/coq/props.mma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Legacy-2 => procedural/lambdadelta/legacy_1}/preamble.ma (100%) rename matita/matita/contribs/{LAMBDA-TYPES/Legacy-2 => procedural/lambdadelta/legacy_1}/theory.ma (100%) rename matita/matita/contribs/{LAMBDA-TYPES => procedural/lambdadelta}/root (100%) diff --git a/matita/matita/contribs/LAMBDA-TYPES/Makefile b/matita/matita/contribs/procedural/lambdadelta/Makefile similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Makefile rename to matita/matita/contribs/procedural/lambdadelta/Makefile diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/A/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/A/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/A/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/A/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/C/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/C/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/C/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/C/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/C/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/C/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/C/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/C/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/G/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/G/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/G/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/G/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/T/dec.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/T/dec.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/T/dec.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/T/dec.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/T/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/T/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/T/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/T/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/T/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/T/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/T/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/T/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/aplus/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/aplus/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/aplus/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/aplus/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/aplus/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/aplus/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/aplus/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/aplus/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/app/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/app/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/app/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/app/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/aprem/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/aprem/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/aprem/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/aprem/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/aprem/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/aprem/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/aprem/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/arity/aprem.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/arity/aprem.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/arity/aprem.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/arity/aprem.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/arity/cimp.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/arity/cimp.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/arity/cimp.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/arity/cimp.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/arity/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/arity/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/arity/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/arity/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/arity/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/arity/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/arity/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/arity/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/arity/lift1.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/arity/lift1.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/arity/lift1.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/arity/lift1.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/arity/pr3.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/arity/pr3.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/arity/pr3.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/arity/pr3.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/arity/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/arity/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/arity/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/arity/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/arity/subst0.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/arity/subst0.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/arity/subst0.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/arity/subst0.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/asucc/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/asucc/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/asucc/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/asucc/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/asucc/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/asucc/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/asucc/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/asucc/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/cimp/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/cimp/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/cimp/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/cimp/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/cimp/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/cimp/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/cimp/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/cimp/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/clear/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/clear/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/clear/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/clear/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/clear/drop.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/clear/drop.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/clear/drop.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/clear/drop.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/clear/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/clear/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/clear/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/clear/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/clear/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/clear/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/clear/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/clear/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/clen/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/clen/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/clen/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/clen/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/clen/getl.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/clen/getl.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/clen/getl.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/clen/getl.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/cnt/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/cnt/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/cnt/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/cnt/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/cnt/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/cnt/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/cnt/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/cnt/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/arity.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csuba/arity.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/arity.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csuba/arity.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/clear.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csuba/clear.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/clear.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csuba/clear.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csuba/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csuba/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/drop.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csuba/drop.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/drop.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csuba/drop.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csuba/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csuba/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/getl.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csuba/getl.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/getl.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csuba/getl.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csuba/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csuba/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csuba/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/arity.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubc/arity.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/arity.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubc/arity.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/clear.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubc/clear.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/clear.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubc/clear.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/csuba.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubc/csuba.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/csuba.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubc/csuba.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubc/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubc/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/drop.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubc/drop.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/drop.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubc/drop.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/drop1.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubc/drop1.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/drop1.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubc/drop1.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubc/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubc/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/getl.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubc/getl.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/getl.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubc/getl.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubc/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubc/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubc/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/clear.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubst0/clear.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/clear.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubst0/clear.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubst0/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubst0/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/drop.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubst0/drop.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/drop.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubst0/drop.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubst0/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubst0/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/getl.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubst0/getl.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/getl.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubst0/getl.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubst0/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubst0/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubst0/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubst1/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubst1/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubst1/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubst1/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/getl.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubst1/getl.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/getl.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubst1/getl.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubst1/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubst1/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubst1/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/clear.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubt/clear.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/clear.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubt/clear.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/csuba.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubt/csuba.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/csuba.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubt/csuba.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubt/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubt/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/drop.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubt/drop.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/drop.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubt/drop.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubt/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubt/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/getl.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubt/getl.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/getl.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubt/getl.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/pc3.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubt/pc3.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/pc3.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubt/pc3.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubt/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubt/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/ty3.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubt/ty3.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubt/ty3.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubt/ty3.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/clear.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubv/clear.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/clear.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubv/clear.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubv/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubv/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/drop.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubv/drop.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/drop.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubv/drop.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/getl.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubv/getl.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/getl.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubv/getl.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/csubv/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/csubv/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/csubv/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/drop/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/drop/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/drop/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/drop/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/drop/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/drop/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/drop/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/drop/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/drop/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/drop/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/drop/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/drop/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/drop1/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/drop1/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/drop1/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/drop1/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/getl.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/drop1/getl.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/getl.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/drop1/getl.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/drop1/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/drop1/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/drop1/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/ex0/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/ex0/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/ex0/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/ex0/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/ex0/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/ex0/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/ex0/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/ex0/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/ex1/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/ex1/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/ex1/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/ex1/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/ex1/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/ex1/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/ex1/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/ex1/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/ex2/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/ex2/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/ex2/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/ex2/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/ex2/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/ex2/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/ex2/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/ex2/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/flt/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/flt/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/flt/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/flt/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/flt/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/flt/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/flt/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/flt/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/fsubst0/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/fsubst0/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/fsubst0/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/fsubst0/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/fsubst0/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/fsubst0/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/fsubst0/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/fsubst0/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/getl/clear.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/getl/clear.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/getl/clear.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/getl/clear.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/getl/dec.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/getl/dec.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/getl/dec.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/getl/dec.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/getl/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/getl/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/getl/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/getl/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/getl/drop.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/getl/drop.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/getl/drop.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/getl/drop.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/getl/flt.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/getl/flt.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/getl/flt.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/getl/flt.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/getl/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/getl/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/getl/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/getl/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/getl/getl.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/getl/getl.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/getl/getl.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/getl/getl.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/getl/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/getl/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/getl/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/getl/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/iso/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/iso/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/iso/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/iso/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/iso/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/iso/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/iso/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/iso/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/iso/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/iso/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/iso/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/iso/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/leq/asucc.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/leq/asucc.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/leq/asucc.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/leq/asucc.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/leq/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/leq/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/leq/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/leq/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/leq/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/leq/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/leq/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/leq/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/leq/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/leq/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/leq/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/leq/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/lift/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/lift/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/lift/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/lift/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/lift/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/lift/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/lift/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/lift/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/lift/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/lift/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/lift/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/lift/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/lift/tlt.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/lift/tlt.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/lift/tlt.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/lift/tlt.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/lift1/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/lift1/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/lift1/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/lift1/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/lift1/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/lift1/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/lift1/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/llt/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/llt/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/llt/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/llt/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/llt/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/llt/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/llt/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/llt/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/next_plus/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/next_plus/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/next_plus/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/next_plus/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/next_plus/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/next_plus/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/next_plus/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/next_plus/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/arity.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/nf2/arity.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/arity.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/nf2/arity.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/dec.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/nf2/dec.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/dec.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/nf2/dec.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/nf2/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/nf2/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/nf2/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/nf2/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/iso.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/nf2/iso.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/iso.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/nf2/iso.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/lift1.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/nf2/lift1.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/lift1.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/nf2/lift1.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/pr3.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/nf2/pr3.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/pr3.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/nf2/pr3.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/nf2/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/nf2/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/nf2/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc1/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pc1/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc1/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pc1/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc1/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pc1/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc1/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pc1/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/dec.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pc3/dec.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/dec.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pc3/dec.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pc3/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pc3/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/fsubst0.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pc3/fsubst0.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/fsubst0.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pc3/fsubst0.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pc3/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pc3/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/left.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pc3/left.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/left.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pc3/left.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/nf2.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pc3/nf2.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/nf2.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pc3/nf2.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/pc1.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pc3/pc1.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/pc1.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pc3/pc1.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pc3/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pc3/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/subst1.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pc3/subst1.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/subst1.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pc3/subst1.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/wcpr0.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pc3/wcpr0.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pc3/wcpr0.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pc3/wcpr0.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/dec.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr0/dec.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/dec.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr0/dec.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr0/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr0/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr0/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr0/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/pr0.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr0/pr0.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/pr0.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr0/pr0.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr0/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr0/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/subst1.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr0/subst1.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr0/subst1.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr0/subst1.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr1/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr1/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/pr1.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr1/pr1.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/pr1.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr1/pr1.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr1/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr1/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr1/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/clen.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr2/clen.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/clen.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr2/clen.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr2/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr2/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr2/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr2/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/pr2.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr2/pr2.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/pr2.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr2/pr2.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr2/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr2/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/subst1.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr2/subst1.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr2/subst1.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr2/subst1.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr3/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr3/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr3/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr3/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/iso.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr3/iso.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/iso.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr3/iso.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/pr1.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr3/pr1.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/pr1.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr3/pr1.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/pr3.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr3/pr3.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/pr3.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr3/pr3.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr3/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr3/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/subst1.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr3/subst1.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/subst1.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr3/subst1.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/wcpr0.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/pr3/wcpr0.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/pr3/wcpr0.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/pr3/wcpr0.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/preamble.ma b/matita/matita/contribs/procedural/lambdadelta/basic_1/preamble.ma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/preamble.ma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/preamble.ma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/r/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/r/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/r/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/r/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/r/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/r/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/r/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/r/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/s/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/s/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/s/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/s/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/s/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/s/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/s/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/s/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/arity.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/sc3/arity.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/arity.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/sc3/arity.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/sc3/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/sc3/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/sc3/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/sc3/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/sc3/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/sn3/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/sn3/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/sn3/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/sn3/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/lift1.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/sn3/lift1.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/lift1.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/sn3/lift1.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/nf2.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/sn3/nf2.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/nf2.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/sn3/nf2.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/sn3/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/sn3/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/sn3/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/sty0/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/sty0/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/sty0/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/sty0/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/sty0/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/sty0/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/sty0/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/cnt.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/sty1/cnt.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/cnt.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/sty1/cnt.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/sty1/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/sty1/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/sty1/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/sty1/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/sty1/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/subst/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/subst/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/subst/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/subst/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/subst/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/subst/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/dec.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/subst0/dec.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/dec.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/subst0/dec.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/subst0/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/subst0/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/subst0/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/subst0/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/subst0/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/subst0/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/subst0.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/subst0/subst0.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/subst0.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/subst0/subst0.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/tlt.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/subst0/tlt.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst0/tlt.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/subst0/tlt.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/subst1/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/subst1/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/subst1/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/subst1/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/subst1/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/subst1/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/subst1.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/subst1/subst1.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/subst1/subst1.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/subst1/subst1.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/theory.ma b/matita/matita/contribs/procedural/lambdadelta/basic_1/theory.ma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/theory.ma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/theory.ma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/tlist/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/tlist/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/tlist/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/tlist/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/tlist/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/tlist/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/tlist/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/tlist/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/tlt/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/tlt/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/tlt/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/tlt/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/tlt/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/tlt/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/tlt/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/tlt/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/arity.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/arity.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/arity.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/arity.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/arity_props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/arity_props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/arity_props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/arity_props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/dec.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/dec.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/dec.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/dec.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fsubst0.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/fsubst0.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fsubst0.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/fsubst0.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fwd_nf2.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/fwd_nf2.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/fwd_nf2.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/fwd_nf2.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/nf2.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/nf2.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/nf2.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/nf2.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/pr3.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/pr3.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/pr3.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/pr3.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/pr3_props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/pr3_props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/pr3_props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/pr3_props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/sty0.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/sty0.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/sty0.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/sty0.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/subst1.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/subst1.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/ty3/subst1.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/ty3/subst1.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/wcpr0/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/wcpr0/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/wcpr0/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/wcpr0/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/getl.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/wcpr0/getl.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/wcpr0/getl.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/wcpr0/getl.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/clear.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/wf3/clear.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/clear.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/wf3/clear.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/defs.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/wf3/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/wf3/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/fwd.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/wf3/fwd.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/fwd.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/wf3/fwd.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/getl.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/wf3/getl.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/getl.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/wf3/getl.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/props.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/wf3/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/props.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/wf3/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/ty3.mma b/matita/matita/contribs/procedural/lambdadelta/basic_1/wf3/ty3.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Basic-2/wf3/ty3.mma rename to matita/matita/contribs/procedural/lambdadelta/basic_1/wf3/ty3.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/depends b/matita/matita/contribs/procedural/lambdadelta/depends similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/depends rename to matita/matita/contribs/procedural/lambdadelta/depends diff --git a/matita/matita/contribs/LAMBDA-TYPES/Ground-2/blt/defs.mma b/matita/matita/contribs/procedural/lambdadelta/ground_1/blt/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Ground-2/blt/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/ground_1/blt/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Ground-2/blt/props.mma b/matita/matita/contribs/procedural/lambdadelta/ground_1/blt/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Ground-2/blt/props.mma rename to matita/matita/contribs/procedural/lambdadelta/ground_1/blt/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Ground-2/ext/arith.mma b/matita/matita/contribs/procedural/lambdadelta/ground_1/ext/arith.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Ground-2/ext/arith.mma rename to matita/matita/contribs/procedural/lambdadelta/ground_1/ext/arith.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Ground-2/ext/tactics.mma b/matita/matita/contribs/procedural/lambdadelta/ground_1/ext/tactics.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Ground-2/ext/tactics.mma rename to matita/matita/contribs/procedural/lambdadelta/ground_1/ext/tactics.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Ground-2/plist/defs.mma b/matita/matita/contribs/procedural/lambdadelta/ground_1/plist/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Ground-2/plist/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/ground_1/plist/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Ground-2/plist/props.mma b/matita/matita/contribs/procedural/lambdadelta/ground_1/plist/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Ground-2/plist/props.mma rename to matita/matita/contribs/procedural/lambdadelta/ground_1/plist/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Ground-2/preamble.ma b/matita/matita/contribs/procedural/lambdadelta/ground_1/preamble.ma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Ground-2/preamble.ma rename to matita/matita/contribs/procedural/lambdadelta/ground_1/preamble.ma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Ground-2/theory.ma b/matita/matita/contribs/procedural/lambdadelta/ground_1/theory.ma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Ground-2/theory.ma rename to matita/matita/contribs/procedural/lambdadelta/ground_1/theory.ma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Ground-2/types/defs.mma b/matita/matita/contribs/procedural/lambdadelta/ground_1/types/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Ground-2/types/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/ground_1/types/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Ground-2/types/props.mma b/matita/matita/contribs/procedural/lambdadelta/ground_1/types/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Ground-2/types/props.mma rename to matita/matita/contribs/procedural/lambdadelta/ground_1/types/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Legacy-2/coq/defs.mma b/matita/matita/contribs/procedural/lambdadelta/legacy_1/coq/defs.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Legacy-2/coq/defs.mma rename to matita/matita/contribs/procedural/lambdadelta/legacy_1/coq/defs.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Legacy-2/coq/props.mma b/matita/matita/contribs/procedural/lambdadelta/legacy_1/coq/props.mma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Legacy-2/coq/props.mma rename to matita/matita/contribs/procedural/lambdadelta/legacy_1/coq/props.mma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma b/matita/matita/contribs/procedural/lambdadelta/legacy_1/preamble.ma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Legacy-2/preamble.ma rename to matita/matita/contribs/procedural/lambdadelta/legacy_1/preamble.ma diff --git a/matita/matita/contribs/LAMBDA-TYPES/Legacy-2/theory.ma b/matita/matita/contribs/procedural/lambdadelta/legacy_1/theory.ma similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/Legacy-2/theory.ma rename to matita/matita/contribs/procedural/lambdadelta/legacy_1/theory.ma diff --git a/matita/matita/contribs/LAMBDA-TYPES/root b/matita/matita/contribs/procedural/lambdadelta/root similarity index 100% rename from matita/matita/contribs/LAMBDA-TYPES/root rename to matita/matita/contribs/procedural/lambdadelta/root -- 2.39.2