From 14d370851b7779e9fc6343532372e939dadb831c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 7 Feb 2007 18:34:04 +0000 Subject: [PATCH] refactoring --- .../{Base-1 => }/Base/blt/defs.ma | 0 .../{Base-1 => }/Base/blt/props.ma | 0 .../{Base-1 => }/Base/ext/arith.ma | 0 .../{Base-1 => }/Base/ext/tactics.ma | 0 .../LAMBDA-TYPES/{Base-1 => }/Base/makefile | 0 .../{Base-1 => }/Base/plist/defs.ma | 0 .../{Base-1 => }/Base/plist/props.ma | 0 .../{Base-1 => }/Base/preamble.ma | 0 .../LAMBDA-TYPES/{Base-1 => }/Base/spare.ma | 0 .../LAMBDA-TYPES/{Base-1 => }/Base/theory.ma | 0 .../{Base-1 => }/Base/types/defs.ma | 0 .../{Base-1 => }/Base/types/props.ma | 0 .../LambdaDelta => LambdaDelta-1}/A/defs.ma | 0 .../LambdaDelta => LambdaDelta-1}/C/defs.ma | 0 .../LambdaDelta => LambdaDelta-1}/C/props.ma | 0 .../LambdaDelta => LambdaDelta-1}/G/defs.ma | 0 .../LambdaDelta => LambdaDelta-1}/T/dec.ma | 0 .../LambdaDelta => LambdaDelta-1}/T/defs.ma | 0 .../LambdaDelta => LambdaDelta-1}/T/props.ma | 0 .../aplus/defs.ma | 0 .../aplus/props.ma | 0 .../aprem/defs.ma | 0 .../aprem/props.ma | 0 .../arity/aprem.ma | 0 .../arity/cimp.ma | 0 .../arity/defs.ma | 0 .../arity/fwd.ma | 0 .../arity/lift1.ma | 0 .../arity/pr3.ma | 0 .../arity/props.ma | 0 .../arity/subst0.ma | 0 .../asucc/defs.ma | 0 .../asucc/fwd.ma | 0 .../cimp/defs.ma | 0 .../cimp/props.ma | 0 .../clear/defs.ma | 0 .../clear/drop.ma | 0 .../clear/fwd.ma | 0 .../clear/props.ma | 0 .../clen/defs.ma | 0 .../clen/getl.ma | 0 .../LambdaDelta => LambdaDelta-1}/cnt/defs.ma | 0 .../cnt/props.ma | 0 .../csuba/arity.ma | 0 .../csuba/clear.ma | 0 .../csuba/defs.ma | 0 .../csuba/drop.ma | 0 .../csuba/fwd.ma | 0 .../csuba/getl.ma | 0 .../csuba/props.ma | 0 .../csubc/arity.ma | 0 .../csubc/clear.ma | 0 .../csubc/csuba.ma | 0 .../csubc/defs.ma | 0 .../csubc/drop.ma | 0 .../csubc/drop1.ma | 0 .../csubc/getl.ma | 0 .../csubc/props.ma | 0 .../csubst0/clear.ma | 0 .../csubst0/defs.ma | 0 .../csubst0/drop.ma | 0 .../csubst0/fwd.ma | 0 .../csubst0/getl.ma | 0 .../csubst0/props.ma | 0 .../csubst1/defs.ma | 0 .../csubst1/fwd.ma | 0 .../csubst1/getl.ma | 0 .../csubst1/props.ma | 0 .../csubt/clear.ma | 0 .../csubt/defs.ma | 0 .../csubt/drop.ma | 0 .../csubt/fwd.ma | 0 .../csubt/getl.ma | 0 .../csubt/pc3.ma | 0 .../csubt/props.ma | 0 .../csubt/ty3.ma | 0 .../drop/defs.ma | 0 .../LambdaDelta => LambdaDelta-1}/drop/fwd.ma | 0 .../drop/props.ma | 0 .../drop1/defs.ma | 0 .../drop1/getl.ma | 0 .../drop1/props.ma | 0 .../LambdaDelta => LambdaDelta-1}/ex1/defs.ma | 0 .../ex1/props.ma | 0 .../LambdaDelta => LambdaDelta-1}/flt/defs.ma | 0 .../flt/props.ma | 0 .../fsubst0/defs.ma | 0 .../fsubst0/fwd.ma | 0 .../getl/clear.ma | 0 .../LambdaDelta => LambdaDelta-1}/getl/dec.ma | 0 .../getl/defs.ma | 0 .../getl/drop.ma | 0 .../LambdaDelta => LambdaDelta-1}/getl/flt.ma | 0 .../LambdaDelta => LambdaDelta-1}/getl/fwd.ma | 0 .../getl/getl.ma | 0 .../getl/props.ma | 0 .../LambdaDelta => LambdaDelta-1}/gz/defs.ma | 0 .../LambdaDelta => LambdaDelta-1}/gz/props.ma | 0 .../LambdaDelta => LambdaDelta-1}/iso/defs.ma | 0 .../LambdaDelta => LambdaDelta-1}/iso/fwd.ma | 0 .../iso/props.ma | 0 .../leq/asucc.ma | 0 .../LambdaDelta => LambdaDelta-1}/leq/defs.ma | 0 .../LambdaDelta => LambdaDelta-1}/leq/fwd.ma | 0 .../leq/props.ma | 0 .../lift/defs.ma | 0 .../LambdaDelta => LambdaDelta-1}/lift/fwd.ma | 0 .../lift/props.ma | 0 .../LambdaDelta => LambdaDelta-1}/lift/tlt.ma | 0 .../lift1/defs.ma | 0 .../lift1/fwd.ma | 0 .../lift1/props.ma | 0 .../LambdaDelta => LambdaDelta-1}/llt/defs.ma | 0 .../llt/props.ma | 0 .../{Level-1/Base => LambdaDelta-1}/makefile | 0 .../next_plus/defs.ma | 0 .../next_plus/props.ma | 0 .../LambdaDelta => LambdaDelta-1}/nf2/dec.ma | 0 .../LambdaDelta => LambdaDelta-1}/nf2/defs.ma | 0 .../LambdaDelta => LambdaDelta-1}/nf2/fwd.ma | 0 .../LambdaDelta => LambdaDelta-1}/nf2/iso.ma | 0 .../nf2/lift1.ma | 0 .../LambdaDelta => LambdaDelta-1}/nf2/pr3.ma | 0 .../nf2/props.ma | 0 .../LambdaDelta => LambdaDelta-1}/pc1/defs.ma | 0 .../pc1/props.ma | 0 .../LambdaDelta => LambdaDelta-1}/pc3/dec.ma | 0 .../LambdaDelta => LambdaDelta-1}/pc3/defs.ma | 0 .../pc3/fsubst0.ma | 0 .../LambdaDelta => LambdaDelta-1}/pc3/fwd.ma | 0 .../LambdaDelta => LambdaDelta-1}/pc3/left.ma | 0 .../LambdaDelta => LambdaDelta-1}/pc3/pc1.ma | 0 .../pc3/props.ma | 0 .../pc3/subst1.ma | 0 .../pc3/wcpr0.ma | 0 .../LambdaDelta => LambdaDelta-1}/pr0/dec.ma | 0 .../LambdaDelta => LambdaDelta-1}/pr0/defs.ma | 0 .../LambdaDelta => LambdaDelta-1}/pr0/fwd.ma | 0 .../LambdaDelta => LambdaDelta-1}/pr0/pr0.ma | 0 .../pr0/props.ma | 0 .../pr0/subst1.ma | 0 .../LambdaDelta => LambdaDelta-1}/pr1/defs.ma | 0 .../LambdaDelta => LambdaDelta-1}/pr1/pr1.ma | 0 .../pr1/props.ma | 0 .../LambdaDelta => LambdaDelta-1}/pr2/clen.ma | 0 .../LambdaDelta => LambdaDelta-1}/pr2/defs.ma | 0 .../LambdaDelta => LambdaDelta-1}/pr2/fwd.ma | 0 .../LambdaDelta => LambdaDelta-1}/pr2/pr2.ma | 0 .../pr2/props.ma | 0 .../pr2/subst1.ma | 0 .../LambdaDelta => LambdaDelta-1}/pr3/defs.ma | 0 .../LambdaDelta => LambdaDelta-1}/pr3/fwd.ma | 0 .../LambdaDelta => LambdaDelta-1}/pr3/iso.ma | 0 .../LambdaDelta => LambdaDelta-1}/pr3/pr1.ma | 0 .../LambdaDelta => LambdaDelta-1}/pr3/pr3.ma | 0 .../pr3/props.ma | 0 .../pr3/subst1.ma | 0 .../pr3/wcpr0.ma | 0 .../LambdaDelta => LambdaDelta-1}/preamble.ma | 0 .../LambdaDelta => LambdaDelta-1}/r/defs.ma | 0 .../LambdaDelta => LambdaDelta-1}/r/props.ma | 0 .../LambdaDelta => LambdaDelta-1}/s/defs.ma | 0 .../LambdaDelta => LambdaDelta-1}/s/props.ma | 0 .../sc3/arity.ma | 0 .../LambdaDelta => LambdaDelta-1}/sc3/defs.ma | 0 .../sc3/props.ma | 0 .../LambdaDelta => LambdaDelta-1}/sn3/defs.ma | 0 .../LambdaDelta => LambdaDelta-1}/sn3/fwd.ma | 0 .../sn3/lift1.ma | 0 .../LambdaDelta => LambdaDelta-1}/sn3/nf2.ma | 0 .../sn3/props.ma | 0 .../LambdaDelta => LambdaDelta-1}/spare.ma | 0 .../subst0/dec.ma | 0 .../subst0/defs.ma | 0 .../subst0/fwd.ma | 0 .../subst0/props.ma | 0 .../subst0/subst0.ma | 0 .../subst0/tlt.ma | 0 .../subst1/defs.ma | 0 .../subst1/fwd.ma | 0 .../subst1/props.ma | 0 .../subst1/subst1.ma | 0 .../tau0/defs.ma | 0 .../tau0/props.ma | 0 .../LambdaDelta => LambdaDelta-1}/tau1/cnt.ma | 0 .../tau1/defs.ma | 0 .../tau1/props.ma | 0 .../LambdaDelta => LambdaDelta-1}/theory.ma | 0 .../tlist/defs.ma | 0 .../tlist/props.ma | 0 .../LambdaDelta => LambdaDelta-1}/tlt/defs.ma | 0 .../tlt/props.ma | 0 .../ty3/arity.ma | 0 .../ty3/arity_props.ma | 0 .../LambdaDelta => LambdaDelta-1}/ty3/dec.ma | 0 .../LambdaDelta => LambdaDelta-1}/ty3/defs.ma | 0 .../ty3/fsubst0.ma | 0 .../LambdaDelta => LambdaDelta-1}/ty3/fwd.ma | 0 .../LambdaDelta => LambdaDelta-1}/ty3/pr3.ma | 0 .../ty3/pr3_props.ma | 0 .../ty3/props.ma | 0 .../ty3/subst1.ma | 0 .../LambdaDelta => LambdaDelta-1}/ty3/tau0.ma | 0 .../wcpr0/defs.ma | 0 .../wcpr0/fwd.ma | 0 .../wcpr0/getl.ma | 0 .../LAMBDA-TYPES/Level-1/Base/blt/defs.ma | 27 - .../LAMBDA-TYPES/Level-1/Base/blt/props.ma | 102 --- .../LAMBDA-TYPES/Level-1/Base/ext/arith.ma | 588 ------------------ .../LAMBDA-TYPES/Level-1/Base/ext/tactics.ma | 42 -- .../LAMBDA-TYPES/Level-1/Base/plist/defs.ma | 45 -- .../LAMBDA-TYPES/Level-1/Base/plist/props.ma | 33 - .../LAMBDA-TYPES/Level-1/Base/preamble.ma | 160 ----- .../LAMBDA-TYPES/Level-1/Base/spare.ma | 20 - .../LAMBDA-TYPES/Level-1/Base/theory.ma | 28 - .../LAMBDA-TYPES/Level-1/Base/types/defs.ma | 150 ----- .../LAMBDA-TYPES/Level-1/Base/types/props.ma | 32 - .../LAMBDA-TYPES/Level-1/LambdaDelta/makefile | 39 -- 218 files changed, 1266 deletions(-) rename matita/contribs/LAMBDA-TYPES/{Base-1 => }/Base/blt/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Base-1 => }/Base/blt/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Base-1 => }/Base/ext/arith.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Base-1 => }/Base/ext/tactics.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Base-1 => }/Base/makefile (100%) rename matita/contribs/LAMBDA-TYPES/{Base-1 => }/Base/plist/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Base-1 => }/Base/plist/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Base-1 => }/Base/preamble.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Base-1 => }/Base/spare.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Base-1 => }/Base/theory.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Base-1 => }/Base/types/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Base-1 => }/Base/types/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/A/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/C/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/C/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/G/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/T/dec.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/T/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/T/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/aplus/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/aplus/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/aprem/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/aprem/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/arity/aprem.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/arity/cimp.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/arity/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/arity/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/arity/lift1.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/arity/pr3.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/arity/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/arity/subst0.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/asucc/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/asucc/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/cimp/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/cimp/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/clear/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/clear/drop.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/clear/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/clear/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/clen/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/clen/getl.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/cnt/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/cnt/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csuba/arity.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csuba/clear.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csuba/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csuba/drop.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csuba/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csuba/getl.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csuba/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubc/arity.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubc/clear.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubc/csuba.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubc/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubc/drop.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubc/drop1.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubc/getl.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubc/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubst0/clear.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubst0/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubst0/drop.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubst0/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubst0/getl.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubst0/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubst1/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubst1/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubst1/getl.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubst1/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubt/clear.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubt/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubt/drop.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubt/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubt/getl.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubt/pc3.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubt/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/csubt/ty3.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/drop/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/drop/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/drop/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/drop1/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/drop1/getl.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/drop1/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/ex1/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/ex1/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/flt/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/flt/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/fsubst0/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/fsubst0/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/getl/clear.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/getl/dec.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/getl/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/getl/drop.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/getl/flt.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/getl/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/getl/getl.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/getl/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/gz/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/gz/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/iso/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/iso/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/iso/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/leq/asucc.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/leq/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/leq/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/leq/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/lift/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/lift/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/lift/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/lift/tlt.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/lift1/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/lift1/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/lift1/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/llt/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/llt/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/Base => LambdaDelta-1}/makefile (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/next_plus/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/next_plus/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/nf2/dec.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/nf2/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/nf2/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/nf2/iso.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/nf2/lift1.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/nf2/pr3.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/nf2/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pc1/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pc1/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pc3/dec.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pc3/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pc3/fsubst0.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pc3/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pc3/left.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pc3/pc1.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pc3/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pc3/subst1.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pc3/wcpr0.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr0/dec.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr0/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr0/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr0/pr0.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr0/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr0/subst1.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr1/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr1/pr1.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr1/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr2/clen.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr2/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr2/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr2/pr2.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr2/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr2/subst1.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr3/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr3/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr3/iso.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr3/pr1.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr3/pr3.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr3/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr3/subst1.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/pr3/wcpr0.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/preamble.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/r/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/r/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/s/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/s/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/sc3/arity.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/sc3/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/sc3/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/sn3/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/sn3/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/sn3/lift1.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/sn3/nf2.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/sn3/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/spare.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/subst0/dec.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/subst0/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/subst0/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/subst0/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/subst0/subst0.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/subst0/tlt.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/subst1/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/subst1/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/subst1/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/subst1/subst1.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/tau0/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/tau0/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/tau1/cnt.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/tau1/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/tau1/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/theory.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/tlist/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/tlist/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/tlt/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/tlt/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/ty3/arity.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/ty3/arity_props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/ty3/dec.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/ty3/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/ty3/fsubst0.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/ty3/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/ty3/pr3.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/ty3/pr3_props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/ty3/props.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/ty3/subst1.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/ty3/tau0.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/wcpr0/defs.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/wcpr0/fwd.ma (100%) rename matita/contribs/LAMBDA-TYPES/{Level-1/LambdaDelta => LambdaDelta-1}/wcpr0/getl.ma (100%) delete mode 100644 matita/contribs/LAMBDA-TYPES/Level-1/Base/blt/defs.ma delete mode 100644 matita/contribs/LAMBDA-TYPES/Level-1/Base/blt/props.ma delete mode 100644 matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/arith.ma delete mode 100644 matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/tactics.ma delete mode 100644 matita/contribs/LAMBDA-TYPES/Level-1/Base/plist/defs.ma delete mode 100644 matita/contribs/LAMBDA-TYPES/Level-1/Base/plist/props.ma delete mode 100644 matita/contribs/LAMBDA-TYPES/Level-1/Base/preamble.ma delete mode 100644 matita/contribs/LAMBDA-TYPES/Level-1/Base/spare.ma delete mode 100644 matita/contribs/LAMBDA-TYPES/Level-1/Base/theory.ma delete mode 100644 matita/contribs/LAMBDA-TYPES/Level-1/Base/types/defs.ma delete mode 100644 matita/contribs/LAMBDA-TYPES/Level-1/Base/types/props.ma delete mode 100644 matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/makefile diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/Base/blt/defs.ma b/matita/contribs/LAMBDA-TYPES/Base/blt/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Base-1/Base/blt/defs.ma rename to matita/contribs/LAMBDA-TYPES/Base/blt/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/Base/blt/props.ma b/matita/contribs/LAMBDA-TYPES/Base/blt/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Base-1/Base/blt/props.ma rename to matita/contribs/LAMBDA-TYPES/Base/blt/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/Base/ext/arith.ma b/matita/contribs/LAMBDA-TYPES/Base/ext/arith.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Base-1/Base/ext/arith.ma rename to matita/contribs/LAMBDA-TYPES/Base/ext/arith.ma diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/Base/ext/tactics.ma b/matita/contribs/LAMBDA-TYPES/Base/ext/tactics.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Base-1/Base/ext/tactics.ma rename to matita/contribs/LAMBDA-TYPES/Base/ext/tactics.ma diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/Base/makefile b/matita/contribs/LAMBDA-TYPES/Base/makefile similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Base-1/Base/makefile rename to matita/contribs/LAMBDA-TYPES/Base/makefile diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/Base/plist/defs.ma b/matita/contribs/LAMBDA-TYPES/Base/plist/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Base-1/Base/plist/defs.ma rename to matita/contribs/LAMBDA-TYPES/Base/plist/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/Base/plist/props.ma b/matita/contribs/LAMBDA-TYPES/Base/plist/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Base-1/Base/plist/props.ma rename to matita/contribs/LAMBDA-TYPES/Base/plist/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/Base/preamble.ma b/matita/contribs/LAMBDA-TYPES/Base/preamble.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Base-1/Base/preamble.ma rename to matita/contribs/LAMBDA-TYPES/Base/preamble.ma diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/Base/spare.ma b/matita/contribs/LAMBDA-TYPES/Base/spare.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Base-1/Base/spare.ma rename to matita/contribs/LAMBDA-TYPES/Base/spare.ma diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/Base/theory.ma b/matita/contribs/LAMBDA-TYPES/Base/theory.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Base-1/Base/theory.ma rename to matita/contribs/LAMBDA-TYPES/Base/theory.ma diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/Base/types/defs.ma b/matita/contribs/LAMBDA-TYPES/Base/types/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Base-1/Base/types/defs.ma rename to matita/contribs/LAMBDA-TYPES/Base/types/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/Base/types/props.ma b/matita/contribs/LAMBDA-TYPES/Base/types/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Base-1/Base/types/props.ma rename to matita/contribs/LAMBDA-TYPES/Base/types/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/A/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/A/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/A/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/A/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/C/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/C/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/C/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/C/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/G/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/G/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/G/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/G/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/dec.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/dec.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/dec.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/dec.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/T/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/aplus/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/aplus/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/aplus/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/aplus/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/aprem/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/aprem/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/aprem/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/aprem/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/arity/aprem.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/aprem.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/arity/aprem.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/aprem.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/arity/cimp.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/cimp.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/arity/cimp.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/cimp.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/arity/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/arity/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/arity/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/arity/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/arity/lift1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/lift1.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/arity/lift1.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/lift1.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/arity/pr3.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/pr3.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/arity/pr3.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/pr3.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/arity/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/arity/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/arity/subst0.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/subst0.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/arity/subst0.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/subst0.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/asucc/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/asucc/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/asucc/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/asucc/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/cimp/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/cimp/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/cimp/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/cimp/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clear/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clear/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clear/drop.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/drop.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clear/drop.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/drop.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clear/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clear/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clear/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clear/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clen/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clen/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clen/getl.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/getl.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/clen/getl.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/getl.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/cnt/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/cnt/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/cnt/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/cnt/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/arity.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/arity.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/arity.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/arity.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/clear.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/clear.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/clear.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/clear.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/drop.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/drop.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/drop.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/drop.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/getl.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/getl.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/getl.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/getl.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csuba/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/arity.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/arity.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/arity.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/arity.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/clear.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/clear.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/clear.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/clear.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/csuba.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/csuba.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/csuba.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/csuba.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/drop.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/drop.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/drop1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop1.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/drop1.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop1.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/getl.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/getl.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/getl.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/getl.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubc/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubst0/clear.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/clear.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubst0/clear.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/clear.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubst0/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubst0/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubst0/drop.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/drop.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubst0/drop.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/drop.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubst0/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubst0/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubst0/getl.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/getl.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubst0/getl.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/getl.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubst0/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubst0/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubst1/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubst1/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubst1/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubst1/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubst1/getl.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/getl.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubst1/getl.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/getl.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubst1/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubst1/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/clear.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/clear.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/clear.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/clear.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/drop.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/drop.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/drop.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/drop.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/getl.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/getl.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/getl.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/getl.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/pc3.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/pc3.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/pc3.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/pc3.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/ty3.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/csubt/ty3.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/getl.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/getl.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/getl.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/getl.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/drop1/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ex1/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ex1/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ex1/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ex1/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/flt/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/flt/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/flt/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/flt/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/fsubst0/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/fsubst0/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/fsubst0/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/fsubst0/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/clear.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/clear.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/clear.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/clear.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/dec.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/dec.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/dec.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/dec.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/drop.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/drop.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/drop.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/drop.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/flt.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/flt.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/flt.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/flt.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/getl.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/getl.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/getl.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/getl.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/getl/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/gz/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/gz/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/gz/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/gz/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/gz/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/gz/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/gz/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/gz/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/iso/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/leq/asucc.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/asucc.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/leq/asucc.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/asucc.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/leq/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/leq/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/leq/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/leq/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/leq/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/leq/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/tlt.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift/tlt.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/lift1/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/llt/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/llt/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/llt/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/llt/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base/makefile b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/makefile similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/Base/makefile rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/makefile diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/next_plus/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/next_plus/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/next_plus/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/next_plus/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/dec.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/dec.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/dec.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/dec.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/iso.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/iso.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/iso.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/iso.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/lift1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/lift1.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/lift1.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/lift1.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/pr3.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/pr3.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/pr3.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/pr3.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/nf2/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc1/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc1/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc1/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc1/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/dec.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/dec.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/dec.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/dec.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/fsubst0.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fsubst0.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/fsubst0.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fsubst0.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/left.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/left.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/left.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/left.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/pc1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/pc1.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/pc1.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/pc1.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/subst1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/subst1.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/subst1.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/subst1.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/wcpr0.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/wcpr0.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pc3/wcpr0.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/wcpr0.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/dec.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/dec.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/dec.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/dec.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/pr0.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/pr0.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/subst1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/subst1.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr0/subst1.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/subst1.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr1/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr1/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr1/pr1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/pr1.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr1/pr1.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/pr1.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr1/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr1/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr2/clen.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/clen.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr2/clen.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/clen.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr2/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr2/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr2/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr2/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr2/pr2.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/pr2.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr2/pr2.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/pr2.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr2/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr2/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr2/subst1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr2/subst1.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/iso.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/iso.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/iso.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/iso.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/pr1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr1.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/pr1.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr1.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/pr3.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr3.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/pr3.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr3.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/subst1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/subst1.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/subst1.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/subst1.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/wcpr0.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/wcpr0.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/pr3/wcpr0.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/wcpr0.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/preamble.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/preamble.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/r/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/r/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/r/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/r/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/s/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/s/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/s/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/s/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/arity.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/arity.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/arity.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/arity.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sc3/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sn3/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sn3/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sn3/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sn3/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sn3/lift1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/lift1.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sn3/lift1.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/lift1.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sn3/nf2.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/nf2.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sn3/nf2.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/nf2.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sn3/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/sn3/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/spare.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/spare.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/dec.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/dec.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/dec.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/dec.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/subst0.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/subst0.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/subst0.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/subst0.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/tlt.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst0/tlt.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst1/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst1/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst1/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst1/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst1/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst1/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst1/subst1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/subst1.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/subst1/subst1.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/subst1.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tau0/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tau0/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tau0/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tau0/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tau1/cnt.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/cnt.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tau1/cnt.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/cnt.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tau1/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tau1/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tau1/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tau1/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/theory.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tlist/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tlist/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tlist/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tlist/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tlt/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tlt/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tlt/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/tlt/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/arity.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/arity.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/arity_props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/arity_props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/dec.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/dec.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/dec.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/dec.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/fsubst0.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/fsubst0.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/pr3.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/pr3.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/pr3_props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/pr3_props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/props.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/subst1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/subst1.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/tau0.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/ty3/tau0.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/wcpr0/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/defs.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/wcpr0/defs.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/defs.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/wcpr0/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/fwd.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/wcpr0/fwd.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/fwd.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/wcpr0/getl.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/getl.ma similarity index 100% rename from matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/wcpr0/getl.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/getl.ma diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base/blt/defs.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base/blt/defs.ma deleted file mode 100644 index 4864a2c86..000000000 --- a/matita/contribs/LAMBDA-TYPES/Level-1/Base/blt/defs.ma +++ /dev/null @@ -1,27 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/blt/defs". - -include "preamble.ma". - -definition blt: - nat \to (nat \to bool) -\def - let rec blt (m: nat) (n: nat) on n: bool \def (match n with [O \Rightarrow -false | (S n0) \Rightarrow (match m with [O \Rightarrow true | (S m0) -\Rightarrow (blt m0 n0)])]) in blt. - diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base/blt/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base/blt/props.ma deleted file mode 100644 index c7952ebd2..000000000 --- a/matita/contribs/LAMBDA-TYPES/Level-1/Base/blt/props.ma +++ /dev/null @@ -1,102 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/blt/props". - -include "blt/defs.ma". - -theorem lt_blt: - \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq bool (blt y x) true))) -\def - \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((lt y n) \to -(eq bool (blt y n) true)))) (\lambda (y: nat).(\lambda (H: (lt y O)).(let H0 -\def (match H in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat -n O) \to (eq bool (blt y O) true)))) with [le_n \Rightarrow (\lambda (H0: (eq -nat (S y) O)).(let H1 \def (eq_ind nat (S y) (\lambda (e: nat).(match e in -nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) -\Rightarrow True])) I O H0) in (False_ind (eq bool (blt y O) true) H1))) | -(le_S m H0) \Rightarrow (\lambda (H1: (eq nat (S m) O)).((let H2 \def (eq_ind -nat (S m) (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) -with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind -((le (S y) m) \to (eq bool (blt y O) true)) H2)) H0))]) in (H0 (refl_equal -nat O))))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((lt y n) \to -(eq bool (blt y n) true))))).(\lambda (y: nat).(nat_ind (\lambda (n0: -nat).((lt n0 (S n)) \to (eq bool (blt n0 (S n)) true))) (\lambda (_: (lt O (S -n))).(refl_equal bool true)) (\lambda (n0: nat).(\lambda (_: (((lt n0 (S n)) -\to (eq bool (match n0 with [O \Rightarrow true | (S m) \Rightarrow (blt m -n)]) true)))).(\lambda (H1: (lt (S n0) (S n))).(H n0 (le_S_n (S n0) n H1))))) -y)))) x). - -theorem le_bge: - \forall (x: nat).(\forall (y: nat).((le x y) \to (eq bool (blt y x) false))) -\def - \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((le n y) \to -(eq bool (blt y n) false)))) (\lambda (y: nat).(\lambda (_: (le O -y)).(refl_equal bool false))) (\lambda (n: nat).(\lambda (H: ((\forall (y: -nat).((le n y) \to (eq bool (blt y n) false))))).(\lambda (y: nat).(nat_ind -(\lambda (n0: nat).((le (S n) n0) \to (eq bool (blt n0 (S n)) false))) -(\lambda (H0: (le (S n) O)).(let H1 \def (match H0 in le return (\lambda (n0: -nat).(\lambda (_: (le ? n0)).((eq nat n0 O) \to (eq bool (blt O (S n)) -false)))) with [le_n \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def -(eq_ind nat (S n) (\lambda (e: nat).(match e in nat return (\lambda (_: -nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in -(False_ind (eq bool (blt O (S n)) false) H2))) | (le_S m H1) \Rightarrow -(\lambda (H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m) (\lambda (e: -nat).(match e in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False -| (S _) \Rightarrow True])) I O H2) in (False_ind ((le (S n) m) \to (eq bool -(blt O (S n)) false)) H3)) H1))]) in (H1 (refl_equal nat O)))) (\lambda (n0: -nat).(\lambda (_: (((le (S n) n0) \to (eq bool (blt n0 (S n)) -false)))).(\lambda (H1: (le (S n) (S n0))).(H n0 (le_S_n n n0 H1))))) y)))) -x). - -theorem blt_lt: - \forall (x: nat).(\forall (y: nat).((eq bool (blt y x) true) \to (lt y x))) -\def - \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq bool (blt -y n) true) \to (lt y n)))) (\lambda (y: nat).(\lambda (H: (eq bool (blt y O) -true)).(let H0 \def (match H in eq return (\lambda (b: bool).(\lambda (_: (eq -? ? b)).((eq bool b true) \to (lt y O)))) with [refl_equal \Rightarrow -(\lambda (H0: (eq bool (blt y O) true)).(let H1 \def (eq_ind bool (blt y O) -(\lambda (e: bool).(match e in bool return (\lambda (_: bool).Prop) with -[true \Rightarrow False | false \Rightarrow True])) I true H0) in (False_ind -(lt y O) H1)))]) in (H0 (refl_equal bool true))))) (\lambda (n: nat).(\lambda -(H: ((\forall (y: nat).((eq bool (blt y n) true) \to (lt y n))))).(\lambda -(y: nat).(nat_ind (\lambda (n0: nat).((eq bool (blt n0 (S n)) true) \to (lt -n0 (S n)))) (\lambda (_: (eq bool true true)).(le_S_n (S O) (S n) (le_n_S (S -O) (S n) (le_n_S O n (le_O_n n))))) (\lambda (n0: nat).(\lambda (_: (((eq -bool (match n0 with [O \Rightarrow true | (S m) \Rightarrow (blt m n)]) true) -\to (lt n0 (S n))))).(\lambda (H1: (eq bool (blt n0 n) true)).(lt_le_S (S n0) -(S n) (lt_n_S n0 n (H n0 H1)))))) y)))) x). - -theorem bge_le: - \forall (x: nat).(\forall (y: nat).((eq bool (blt y x) false) \to (le x y))) -\def - \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq bool (blt -y n) false) \to (le n y)))) (\lambda (y: nat).(\lambda (_: (eq bool (blt y O) -false)).(le_O_n y))) (\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((eq -bool (blt y n) false) \to (le n y))))).(\lambda (y: nat).(nat_ind (\lambda -(n0: nat).((eq bool (blt n0 (S n)) false) \to (le (S n) n0))) (\lambda (H0: -(eq bool (blt O (S n)) false)).(let H1 \def (match H0 in eq return (\lambda -(b: bool).(\lambda (_: (eq ? ? b)).((eq bool b false) \to (le (S n) O)))) -with [refl_equal \Rightarrow (\lambda (H1: (eq bool (blt O (S n)) -false)).(let H2 \def (eq_ind bool (blt O (S n)) (\lambda (e: bool).(match e -in bool return (\lambda (_: bool).Prop) with [true \Rightarrow True | false -\Rightarrow False])) I false H1) in (False_ind (le (S n) O) H2)))]) in (H1 -(refl_equal bool false)))) (\lambda (n0: nat).(\lambda (_: (((eq bool (blt n0 -(S n)) false) \to (le (S n) n0)))).(\lambda (H1: (eq bool (blt (S n0) (S n)) -false)).(le_S_n (S n) (S n0) (le_n_S (S n) (S n0) (le_n_S n n0 (H n0 -H1))))))) y)))) x). - diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/arith.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/arith.ma deleted file mode 100644 index 1ce93fd7f..000000000 --- a/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/arith.ma +++ /dev/null @@ -1,588 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith". - -include "preamble.ma". - -theorem nat_dec: - \forall (n1: nat).(\forall (n2: nat).(or (eq nat n1 n2) ((eq nat n1 n2) \to -(\forall (P: Prop).P)))) -\def - \lambda (n1: nat).(nat_ind (\lambda (n: nat).(\forall (n2: nat).(or (eq nat -n n2) ((eq nat n n2) \to (\forall (P: Prop).P))))) (\lambda (n2: -nat).(nat_ind (\lambda (n: nat).(or (eq nat O n) ((eq nat O n) \to (\forall -(P: Prop).P)))) (or_introl (eq nat O O) ((eq nat O O) \to (\forall (P: -Prop).P)) (refl_equal nat O)) (\lambda (n: nat).(\lambda (_: (or (eq nat O n) -((eq nat O n) \to (\forall (P: Prop).P)))).(or_intror (eq nat O (S n)) ((eq -nat O (S n)) \to (\forall (P: Prop).P)) (\lambda (H0: (eq nat O (S -n))).(\lambda (P: Prop).(let H1 \def (eq_ind nat O (\lambda (ee: nat).(match -ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) -\Rightarrow False])) I (S n) H0) in (False_ind P H1))))))) n2)) (\lambda (n: -nat).(\lambda (H: ((\forall (n2: nat).(or (eq nat n n2) ((eq nat n n2) \to -(\forall (P: Prop).P)))))).(\lambda (n2: nat).(nat_ind (\lambda (n0: nat).(or -(eq nat (S n) n0) ((eq nat (S n) n0) \to (\forall (P: Prop).P)))) (or_intror -(eq nat (S n) O) ((eq nat (S n) O) \to (\forall (P: Prop).P)) (\lambda (H0: -(eq nat (S n) O)).(\lambda (P: Prop).(let H1 \def (eq_ind nat (S n) (\lambda -(ee: nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow -False | (S _) \Rightarrow True])) I O H0) in (False_ind P H1))))) (\lambda -(n0: nat).(\lambda (H0: (or (eq nat (S n) n0) ((eq nat (S n) n0) \to (\forall -(P: Prop).P)))).(or_ind (eq nat n n0) ((eq nat n n0) \to (\forall (P: -Prop).P)) (or (eq nat (S n) (S n0)) ((eq nat (S n) (S n0)) \to (\forall (P: -Prop).P))) (\lambda (H1: (eq nat n n0)).(let H2 \def (eq_ind_r nat n0 -(\lambda (n3: nat).(or (eq nat (S n) n3) ((eq nat (S n) n3) \to (\forall (P: -Prop).P)))) H0 n H1) in (eq_ind nat n (\lambda (n3: nat).(or (eq nat (S n) (S -n3)) ((eq nat (S n) (S n3)) \to (\forall (P: Prop).P)))) (or_introl (eq nat -(S n) (S n)) ((eq nat (S n) (S n)) \to (\forall (P: Prop).P)) (refl_equal nat -(S n))) n0 H1))) (\lambda (H1: (((eq nat n n0) \to (\forall (P: -Prop).P)))).(or_intror (eq nat (S n) (S n0)) ((eq nat (S n) (S n0)) \to -(\forall (P: Prop).P)) (\lambda (H2: (eq nat (S n) (S n0))).(\lambda (P: -Prop).(let H3 \def (f_equal nat nat (\lambda (e: nat).(match e in nat return -(\lambda (_: nat).nat) with [O \Rightarrow n | (S n3) \Rightarrow n3])) (S n) -(S n0) H2) in (let H4 \def (eq_ind_r nat n0 (\lambda (n3: nat).((eq nat n n3) -\to (\forall (P0: Prop).P0))) H1 n H3) in (let H5 \def (eq_ind_r nat n0 -(\lambda (n3: nat).(or (eq nat (S n) n3) ((eq nat (S n) n3) \to (\forall (P0: -Prop).P0)))) H0 n H3) in (H4 (refl_equal nat n) P)))))))) (H n0)))) n2)))) -n1). - -theorem simpl_plus_r: - \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat (plus m n) -(plus p n)) \to (eq nat m p)))) -\def - \lambda (n: nat).(\lambda (m: nat).(\lambda (p: nat).(\lambda (H: (eq nat -(plus m n) (plus p n))).(plus_reg_l n m p (eq_ind_r nat (plus m n) (\lambda -(n0: nat).(eq nat n0 (plus n p))) (eq_ind_r nat (plus p n) (\lambda (n0: -nat).(eq nat n0 (plus n p))) (sym_eq nat (plus n p) (plus p n) (plus_comm n -p)) (plus m n) H) (plus n m) (plus_comm n m)))))). - -theorem minus_plus_r: - \forall (m: nat).(\forall (n: nat).(eq nat (minus (plus m n) n) m)) -\def - \lambda (m: nat).(\lambda (n: nat).(eq_ind_r nat (plus n m) (\lambda (n0: -nat).(eq nat (minus n0 n) m)) (minus_plus n m) (plus m n) (plus_comm m n))). - -theorem plus_permute_2_in_3: - \forall (x: nat).(\forall (y: nat).(\forall (z: nat).(eq nat (plus (plus x -y) z) (plus (plus x z) y)))) -\def - \lambda (x: nat).(\lambda (y: nat).(\lambda (z: nat).(eq_ind_r nat (plus x -(plus y z)) (\lambda (n: nat).(eq nat n (plus (plus x z) y))) (eq_ind_r nat -(plus z y) (\lambda (n: nat).(eq nat (plus x n) (plus (plus x z) y))) (eq_ind -nat (plus (plus x z) y) (\lambda (n: nat).(eq nat n (plus (plus x z) y))) -(refl_equal nat (plus (plus x z) y)) (plus x (plus z y)) (plus_assoc_reverse -x z y)) (plus y z) (plus_comm y z)) (plus (plus x y) z) (plus_assoc_reverse x -y z)))). - -theorem plus_permute_2_in_3_assoc: - \forall (n: nat).(\forall (h: nat).(\forall (k: nat).(eq nat (plus (plus n -h) k) (plus n (plus k h))))) -\def - \lambda (n: nat).(\lambda (h: nat).(\lambda (k: nat).(eq_ind_r nat (plus -(plus n k) h) (\lambda (n0: nat).(eq nat n0 (plus n (plus k h)))) (eq_ind_r -nat (plus (plus n k) h) (\lambda (n0: nat).(eq nat (plus (plus n k) h) n0)) -(refl_equal nat (plus (plus n k) h)) (plus n (plus k h)) (plus_assoc n k h)) -(plus (plus n h) k) (plus_permute_2_in_3 n h k)))). - -theorem plus_O: - \forall (x: nat).(\forall (y: nat).((eq nat (plus x y) O) \to (land (eq nat -x O) (eq nat y O)))) -\def - \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((eq nat (plus -n y) O) \to (land (eq nat n O) (eq nat y O))))) (\lambda (y: nat).(\lambda -(H: (eq nat (plus O y) O)).(conj (eq nat O O) (eq nat y O) (refl_equal nat O) -H))) (\lambda (n: nat).(\lambda (_: ((\forall (y: nat).((eq nat (plus n y) O) -\to (land (eq nat n O) (eq nat y O)))))).(\lambda (y: nat).(\lambda (H0: (eq -nat (plus (S n) y) O)).(let H1 \def (match H0 in eq return (\lambda (n0: -nat).(\lambda (_: (eq ? ? n0)).((eq nat n0 O) \to (land (eq nat (S n) O) (eq -nat y O))))) with [refl_equal \Rightarrow (\lambda (H1: (eq nat (plus (S n) -y) O)).(let H2 \def (eq_ind nat (plus (S n) y) (\lambda (e: nat).(match e in -nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) -\Rightarrow True])) I O H1) in (False_ind (land (eq nat (S n) O) (eq nat y -O)) H2)))]) in (H1 (refl_equal nat O))))))) x). - -theorem minus_Sx_SO: - \forall (x: nat).(eq nat (minus (S x) (S O)) x) -\def - \lambda (x: nat).(eq_ind nat x (\lambda (n: nat).(eq nat n x)) (refl_equal -nat x) (minus x O) (minus_n_O x)). - -theorem eq_nat_dec: - \forall (i: nat).(\forall (j: nat).(or (not (eq nat i j)) (eq nat i j))) -\def - \lambda (i: nat).(nat_ind (\lambda (n: nat).(\forall (j: nat).(or (not (eq -nat n j)) (eq nat n j)))) (\lambda (j: nat).(nat_ind (\lambda (n: nat).(or -(not (eq nat O n)) (eq nat O n))) (or_intror (not (eq nat O O)) (eq nat O O) -(refl_equal nat O)) (\lambda (n: nat).(\lambda (_: (or (not (eq nat O n)) (eq -nat O n))).(or_introl (not (eq nat O (S n))) (eq nat O (S n)) (O_S n)))) j)) -(\lambda (n: nat).(\lambda (H: ((\forall (j: nat).(or (not (eq nat n j)) (eq -nat n j))))).(\lambda (j: nat).(nat_ind (\lambda (n0: nat).(or (not (eq nat -(S n) n0)) (eq nat (S n) n0))) (or_introl (not (eq nat (S n) O)) (eq nat (S -n) O) (sym_not_eq nat O (S n) (O_S n))) (\lambda (n0: nat).(\lambda (_: (or -(not (eq nat (S n) n0)) (eq nat (S n) n0))).(or_ind (not (eq nat n n0)) (eq -nat n n0) (or (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0))) (\lambda -(H1: (not (eq nat n n0))).(or_introl (not (eq nat (S n) (S n0))) (eq nat (S -n) (S n0)) (not_eq_S n n0 H1))) (\lambda (H1: (eq nat n n0)).(or_intror (not -(eq nat (S n) (S n0))) (eq nat (S n) (S n0)) (f_equal nat nat S n n0 H1))) (H -n0)))) j)))) i). - -theorem neq_eq_e: - \forall (i: nat).(\forall (j: nat).(\forall (P: Prop).((((not (eq nat i j)) -\to P)) \to ((((eq nat i j) \to P)) \to P)))) -\def - \lambda (i: nat).(\lambda (j: nat).(\lambda (P: Prop).(\lambda (H: (((not -(eq nat i j)) \to P))).(\lambda (H0: (((eq nat i j) \to P))).(let o \def -(eq_nat_dec i j) in (or_ind (not (eq nat i j)) (eq nat i j) P H H0 o)))))). - -theorem le_false: - \forall (m: nat).(\forall (n: nat).(\forall (P: Prop).((le m n) \to ((le (S -n) m) \to P)))) -\def - \lambda (m: nat).(nat_ind (\lambda (n: nat).(\forall (n0: nat).(\forall (P: -Prop).((le n n0) \to ((le (S n0) n) \to P))))) (\lambda (n: nat).(\lambda (P: -Prop).(\lambda (_: (le O n)).(\lambda (H0: (le (S n) O)).(let H1 \def (match -H0 in le return (\lambda (n0: nat).(\lambda (_: (le ? n0)).((eq nat n0 O) \to -P))) with [le_n \Rightarrow (\lambda (H1: (eq nat (S n) O)).(let H2 \def -(eq_ind nat (S n) (\lambda (e: nat).(match e in nat return (\lambda (_: -nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in -(False_ind P H2))) | (le_S m0 H1) \Rightarrow (\lambda (H2: (eq nat (S m0) -O)).((let H3 \def (eq_ind nat (S m0) (\lambda (e: nat).(match e in nat return -(\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) -I O H2) in (False_ind ((le (S n) m0) \to P) H3)) H1))]) in (H1 (refl_equal -nat O))))))) (\lambda (n: nat).(\lambda (H: ((\forall (n0: nat).(\forall (P: -Prop).((le n n0) \to ((le (S n0) n) \to P)))))).(\lambda (n0: nat).(nat_ind -(\lambda (n1: nat).(\forall (P: Prop).((le (S n) n1) \to ((le (S n1) (S n)) -\to P)))) (\lambda (P: Prop).(\lambda (H0: (le (S n) O)).(\lambda (_: (le (S -O) (S n))).(let H2 \def (match H0 in le return (\lambda (n1: nat).(\lambda -(_: (le ? n1)).((eq nat n1 O) \to P))) with [le_n \Rightarrow (\lambda (H2: -(eq nat (S n) O)).(let H3 \def (eq_ind nat (S n) (\lambda (e: nat).(match e -in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) -\Rightarrow True])) I O H2) in (False_ind P H3))) | (le_S m0 H2) \Rightarrow -(\lambda (H3: (eq nat (S m0) O)).((let H4 \def (eq_ind nat (S m0) (\lambda -(e: nat).(match e in nat return (\lambda (_: nat).Prop) with [O \Rightarrow -False | (S _) \Rightarrow True])) I O H3) in (False_ind ((le (S n) m0) \to P) -H4)) H2))]) in (H2 (refl_equal nat O)))))) (\lambda (n1: nat).(\lambda (_: -((\forall (P: Prop).((le (S n) n1) \to ((le (S n1) (S n)) \to P))))).(\lambda -(P: Prop).(\lambda (H1: (le (S n) (S n1))).(\lambda (H2: (le (S (S n1)) (S -n))).(H n1 P (le_S_n n n1 H1) (le_S_n (S n1) n H2))))))) n0)))) m). - -theorem le_Sx_x: - \forall (x: nat).((le (S x) x) \to (\forall (P: Prop).P)) -\def - \lambda (x: nat).(\lambda (H: (le (S x) x)).(\lambda (P: Prop).(let H0 \def -le_Sn_n in (False_ind P (H0 x H))))). - -theorem minus_le: - \forall (x: nat).(\forall (y: nat).(le (minus x y) x)) -\def - \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).(le (minus n -y) n))) (\lambda (_: nat).(le_n O)) (\lambda (n: nat).(\lambda (H: ((\forall -(y: nat).(le (minus n y) n)))).(\lambda (y: nat).(nat_ind (\lambda (n0: -nat).(le (minus (S n) n0) (S n))) (le_n (S n)) (\lambda (n0: nat).(\lambda -(_: (le (match n0 with [O \Rightarrow (S n) | (S l) \Rightarrow (minus n l)]) -(S n))).(le_S (minus n n0) n (H n0)))) y)))) x). - -theorem le_plus_minus_sym: - \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat m (plus (minus m n) -n)))) -\def - \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(eq_ind_r nat -(plus n (minus m n)) (\lambda (n0: nat).(eq nat m n0)) (le_plus_minus n m H) -(plus (minus m n) n) (plus_comm (minus m n) n)))). - -theorem le_minus_minus: - \forall (x: nat).(\forall (y: nat).((le x y) \to (\forall (z: nat).((le y z) -\to (le (minus y x) (minus z x)))))) -\def - \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (le x y)).(\lambda (z: -nat).(\lambda (H0: (le y z)).(plus_le_reg_l x (minus y x) (minus z x) -(eq_ind_r nat y (\lambda (n: nat).(le n (plus x (minus z x)))) (eq_ind_r nat -z (\lambda (n: nat).(le y n)) H0 (plus x (minus z x)) (le_plus_minus_r x z -(le_trans x y z H H0))) (plus x (minus y x)) (le_plus_minus_r x y H))))))). - -theorem le_minus_plus: - \forall (z: nat).(\forall (x: nat).((le z x) \to (\forall (y: nat).(eq nat -(minus (plus x y) z) (plus (minus x z) y))))) -\def - \lambda (z: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).((le n x) \to -(\forall (y: nat).(eq nat (minus (plus x y) n) (plus (minus x n) y)))))) -(\lambda (x: nat).(\lambda (H: (le O x)).(let H0 \def (match H in le return -(\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n x) \to (\forall (y: -nat).(eq nat (minus (plus x y) O) (plus (minus x O) y)))))) with [le_n -\Rightarrow (\lambda (H0: (eq nat O x)).(eq_ind nat O (\lambda (n: -nat).(\forall (y: nat).(eq nat (minus (plus n y) O) (plus (minus n O) y)))) -(\lambda (y: nat).(sym_eq nat (plus (minus O O) y) (minus (plus O y) O) -(minus_n_O (plus O y)))) x H0)) | (le_S m H0) \Rightarrow (\lambda (H1: (eq -nat (S m) x)).(eq_ind nat (S m) (\lambda (n: nat).((le O m) \to (\forall (y: -nat).(eq nat (minus (plus n y) O) (plus (minus n O) y))))) (\lambda (_: (le O -m)).(\lambda (y: nat).(refl_equal nat (plus (minus (S m) O) y)))) x H1 H0))]) -in (H0 (refl_equal nat x))))) (\lambda (z0: nat).(\lambda (H: ((\forall (x: -nat).((le z0 x) \to (\forall (y: nat).(eq nat (minus (plus x y) z0) (plus -(minus x z0) y))))))).(\lambda (x: nat).(nat_ind (\lambda (n: nat).((le (S -z0) n) \to (\forall (y: nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n -(S z0)) y))))) (\lambda (H0: (le (S z0) O)).(\lambda (y: nat).(let H1 \def -(match H0 in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O) -\to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))))) with -[le_n \Rightarrow (\lambda (H1: (eq nat (S z0) O)).(let H2 \def (eq_ind nat -(S z0) (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) with -[O \Rightarrow False | (S _) \Rightarrow True])) I O H1) in (False_ind (eq -nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y)) H2))) | (le_S m H1) -\Rightarrow (\lambda (H2: (eq nat (S m) O)).((let H3 \def (eq_ind nat (S m) -(\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) with [O -\Rightarrow False | (S _) \Rightarrow True])) I O H2) in (False_ind ((le (S -z0) m) \to (eq nat (minus (plus O y) (S z0)) (plus (minus O (S z0)) y))) H3)) -H1))]) in (H1 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: (((le (S -z0) n) \to (\forall (y: nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n -(S z0)) y)))))).(\lambda (H1: (le (S z0) (S n))).(\lambda (y: nat).(H n -(le_S_n z0 n H1) y))))) x)))) z). - -theorem le_minus: - \forall (x: nat).(\forall (z: nat).(\forall (y: nat).((le (plus x y) z) \to -(le x (minus z y))))) -\def - \lambda (x: nat).(\lambda (z: nat).(\lambda (y: nat).(\lambda (H: (le (plus -x y) z)).(eq_ind nat (minus (plus x y) y) (\lambda (n: nat).(le n (minus z -y))) (le_minus_minus y (plus x y) (le_plus_r x y) z H) x (minus_plus_r x -y))))). - -theorem le_trans_plus_r: - \forall (x: nat).(\forall (y: nat).(\forall (z: nat).((le (plus x y) z) \to -(le y z)))) -\def - \lambda (x: nat).(\lambda (y: nat).(\lambda (z: nat).(\lambda (H: (le (plus -x y) z)).(le_trans y (plus x y) z (le_plus_r x y) H)))). - -theorem le_gen_S: - \forall (m: nat).(\forall (x: nat).((le (S m) x) \to (ex2 nat (\lambda (n: -nat).(eq nat x (S n))) (\lambda (n: nat).(le m n))))) -\def - \lambda (m: nat).(\lambda (x: nat).(\lambda (H: (le (S m) x)).(let H0 \def -(match H in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n x) -\to (ex2 nat (\lambda (n0: nat).(eq nat x (S n0))) (\lambda (n0: nat).(le m -n0)))))) with [le_n \Rightarrow (\lambda (H0: (eq nat (S m) x)).(eq_ind nat -(S m) (\lambda (n: nat).(ex2 nat (\lambda (n0: nat).(eq nat n (S n0))) -(\lambda (n0: nat).(le m n0)))) (ex_intro2 nat (\lambda (n: nat).(eq nat (S -m) (S n))) (\lambda (n: nat).(le m n)) m (refl_equal nat (S m)) (le_n m)) x -H0)) | (le_S m0 H0) \Rightarrow (\lambda (H1: (eq nat (S m0) x)).(eq_ind nat -(S m0) (\lambda (n: nat).((le (S m) m0) \to (ex2 nat (\lambda (n0: nat).(eq -nat n (S n0))) (\lambda (n0: nat).(le m n0))))) (\lambda (H2: (le (S m) -m0)).(ex_intro2 nat (\lambda (n: nat).(eq nat (S m0) (S n))) (\lambda (n: -nat).(le m n)) m0 (refl_equal nat (S m0)) (le_S_n m m0 (le_S (S m) m0 H2)))) -x H1 H0))]) in (H0 (refl_equal nat x))))). - -theorem lt_x_plus_x_Sy: - \forall (x: nat).(\forall (y: nat).(lt x (plus x (S y)))) -\def - \lambda (x: nat).(\lambda (y: nat).(eq_ind_r nat (plus (S y) x) (\lambda (n: -nat).(lt x n)) (le_S_n (S x) (S (plus y x)) (le_n_S (S x) (S (plus y x)) -(le_n_S x (plus y x) (le_plus_r y x)))) (plus x (S y)) (plus_comm x (S y)))). - -theorem simpl_lt_plus_r: - \forall (p: nat).(\forall (n: nat).(\forall (m: nat).((lt (plus n p) (plus m -p)) \to (lt n m)))) -\def - \lambda (p: nat).(\lambda (n: nat).(\lambda (m: nat).(\lambda (H: (lt (plus -n p) (plus m p))).(plus_lt_reg_l n m p (let H0 \def (eq_ind nat (plus n p) -(\lambda (n0: nat).(lt n0 (plus m p))) H (plus p n) (plus_comm n p)) in (let -H1 \def (eq_ind nat (plus m p) (\lambda (n0: nat).(lt (plus p n) n0)) H0 -(plus p m) (plus_comm m p)) in H1)))))). - -theorem minus_x_Sy: - \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq nat (minus x y) (S -(minus x (S y)))))) -\def - \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((lt y n) \to -(eq nat (minus n y) (S (minus n (S y))))))) (\lambda (y: nat).(\lambda (H: -(lt y O)).(let H0 \def (match H in le return (\lambda (n: nat).(\lambda (_: -(le ? n)).((eq nat n O) \to (eq nat (minus O y) (S (minus O (S y))))))) with -[le_n \Rightarrow (\lambda (H0: (eq nat (S y) O)).(let H1 \def (eq_ind nat (S -y) (\lambda (e: nat).(match e in nat return (\lambda (_: nat).Prop) with [O -\Rightarrow False | (S _) \Rightarrow True])) I O H0) in (False_ind (eq nat -(minus O y) (S (minus O (S y)))) H1))) | (le_S m H0) \Rightarrow (\lambda -(H1: (eq nat (S m) O)).((let H2 \def (eq_ind nat (S m) (\lambda (e: -nat).(match e in nat return (\lambda (_: nat).Prop) with [O \Rightarrow False -| (S _) \Rightarrow True])) I O H1) in (False_ind ((le (S y) m) \to (eq nat -(minus O y) (S (minus O (S y))))) H2)) H0))]) in (H0 (refl_equal nat O))))) -(\lambda (n: nat).(\lambda (H: ((\forall (y: nat).((lt y n) \to (eq nat -(minus n y) (S (minus n (S y)))))))).(\lambda (y: nat).(nat_ind (\lambda (n0: -nat).((lt n0 (S n)) \to (eq nat (minus (S n) n0) (S (minus (S n) (S n0)))))) -(\lambda (_: (lt O (S n))).(eq_ind nat n (\lambda (n0: nat).(eq nat (S n) (S -n0))) (refl_equal nat (S n)) (minus n O) (minus_n_O n))) (\lambda (n0: -nat).(\lambda (_: (((lt n0 (S n)) \to (eq nat (minus (S n) n0) (S (minus (S -n) (S n0))))))).(\lambda (H1: (lt (S n0) (S n))).(let H2 \def (le_S_n (S n0) -n H1) in (H n0 H2))))) y)))) x). - -theorem lt_plus_minus: - \forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus x (minus -y (S x))))))) -\def - \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(le_plus_minus (S -x) y H))). - -theorem lt_plus_minus_r: - \forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus (minus y -(S x)) x))))) -\def - \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(eq_ind_r nat -(plus x (minus y (S x))) (\lambda (n: nat).(eq nat y (S n))) (lt_plus_minus x -y H) (plus (minus y (S x)) x) (plus_comm (minus y (S x)) x)))). - -theorem minus_x_SO: - \forall (x: nat).((lt O x) \to (eq nat x (S (minus x (S O))))) -\def - \lambda (x: nat).(\lambda (H: (lt O x)).(eq_ind nat (minus x O) (\lambda (n: -nat).(eq nat x n)) (eq_ind nat x (\lambda (n: nat).(eq nat x n)) (refl_equal -nat x) (minus x O) (minus_n_O x)) (S (minus x (S O))) (minus_x_Sy x O H))). - -theorem le_x_pred_y: - \forall (y: nat).(\forall (x: nat).((lt x y) \to (le x (pred y)))) -\def - \lambda (y: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).((lt x n) \to -(le x (pred n))))) (\lambda (x: nat).(\lambda (H: (lt x O)).(let H0 \def -(match H in le return (\lambda (n: nat).(\lambda (_: (le ? n)).((eq nat n O) -\to (le x O)))) with [le_n \Rightarrow (\lambda (H0: (eq nat (S x) O)).(let -H1 \def (eq_ind nat (S x) (\lambda (e: nat).(match e in nat return (\lambda -(_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow True])) I O H0) -in (False_ind (le x O) H1))) | (le_S m H0) \Rightarrow (\lambda (H1: (eq nat -(S m) O)).((let H2 \def (eq_ind nat (S m) (\lambda (e: nat).(match e in nat -return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) \Rightarrow -True])) I O H1) in (False_ind ((le (S x) m) \to (le x O)) H2)) H0))]) in (H0 -(refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: ((\forall (x: nat).((lt -x n) \to (le x (pred n)))))).(\lambda (x: nat).(\lambda (H0: (lt x (S -n))).(le_S_n x n H0))))) y). - -theorem lt_le_minus: - \forall (x: nat).(\forall (y: nat).((lt x y) \to (le x (minus y (S O))))) -\def - \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(le_minus x y (S -O) (eq_ind_r nat (plus (S O) x) (\lambda (n: nat).(le n y)) H (plus x (S O)) -(plus_comm x (S O)))))). - -theorem lt_le_e: - \forall (n: nat).(\forall (d: nat).(\forall (P: Prop).((((lt n d) \to P)) -\to ((((le d n) \to P)) \to P)))) -\def - \lambda (n: nat).(\lambda (d: nat).(\lambda (P: Prop).(\lambda (H: (((lt n -d) \to P))).(\lambda (H0: (((le d n) \to P))).(let H1 \def (le_or_lt d n) in -(or_ind (le d n) (lt n d) P H0 H H1)))))). - -theorem lt_eq_e: - \forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P)) -\to ((((eq nat x y) \to P)) \to ((le x y) \to P))))) -\def - \lambda (x: nat).(\lambda (y: nat).(\lambda (P: Prop).(\lambda (H: (((lt x -y) \to P))).(\lambda (H0: (((eq nat x y) \to P))).(\lambda (H1: (le x -y)).(or_ind (lt x y) (eq nat x y) P H H0 (le_lt_or_eq x y H1))))))). - -theorem lt_eq_gt_e: - \forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P)) -\to ((((eq nat x y) \to P)) \to ((((lt y x) \to P)) \to P))))) -\def - \lambda (x: nat).(\lambda (y: nat).(\lambda (P: Prop).(\lambda (H: (((lt x -y) \to P))).(\lambda (H0: (((eq nat x y) \to P))).(\lambda (H1: (((lt y x) -\to P))).(lt_le_e x y P H (\lambda (H2: (le y x)).(lt_eq_e y x P H1 (\lambda -(H3: (eq nat y x)).(H0 (sym_eq nat y x H3))) H2)))))))). - -theorem lt_gen_xS: - \forall (x: nat).(\forall (n: nat).((lt x (S n)) \to (or (eq nat x O) (ex2 -nat (\lambda (m: nat).(eq nat x (S m))) (\lambda (m: nat).(lt m n)))))) -\def - \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (n0: nat).((lt n (S -n0)) \to (or (eq nat n O) (ex2 nat (\lambda (m: nat).(eq nat n (S m))) -(\lambda (m: nat).(lt m n0))))))) (\lambda (n: nat).(\lambda (_: (lt O (S -n))).(or_introl (eq nat O O) (ex2 nat (\lambda (m: nat).(eq nat O (S m))) -(\lambda (m: nat).(lt m n))) (refl_equal nat O)))) (\lambda (n: nat).(\lambda -(_: ((\forall (n0: nat).((lt n (S n0)) \to (or (eq nat n O) (ex2 nat (\lambda -(m: nat).(eq nat n (S m))) (\lambda (m: nat).(lt m n0)))))))).(\lambda (n0: -nat).(\lambda (H0: (lt (S n) (S n0))).(or_intror (eq nat (S n) O) (ex2 nat -(\lambda (m: nat).(eq nat (S n) (S m))) (\lambda (m: nat).(lt m n0))) -(ex_intro2 nat (\lambda (m: nat).(eq nat (S n) (S m))) (\lambda (m: nat).(lt -m n0)) n (refl_equal nat (S n)) (le_S_n (S n) n0 H0))))))) x). - -theorem le_lt_false: - \forall (x: nat).(\forall (y: nat).((le x y) \to ((lt y x) \to (\forall (P: -Prop).P)))) -\def - \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (le x y)).(\lambda (H0: (lt -y x)).(\lambda (P: Prop).(False_ind P (le_not_lt x y H H0)))))). - -theorem lt_neq: - \forall (x: nat).(\forall (y: nat).((lt x y) \to (not (eq nat x y)))) -\def - \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(\lambda (H0: (eq -nat x y)).(let H1 \def (eq_ind nat x (\lambda (n: nat).(lt n y)) H y H0) in -(lt_irrefl y H1))))). - -theorem arith0: - \forall (h2: nat).(\forall (d2: nat).(\forall (n: nat).((le (plus d2 h2) n) -\to (\forall (h1: nat).(le (plus d2 h1) (minus (plus n h1) h2)))))) -\def - \lambda (h2: nat).(\lambda (d2: nat).(\lambda (n: nat).(\lambda (H: (le -(plus d2 h2) n)).(\lambda (h1: nat).(eq_ind nat (minus (plus h2 (plus d2 h1)) -h2) (\lambda (n0: nat).(le n0 (minus (plus n h1) h2))) (le_minus_minus h2 -(plus h2 (plus d2 h1)) (le_plus_l h2 (plus d2 h1)) (plus n h1) (eq_ind_r nat -(plus (plus h2 d2) h1) (\lambda (n0: nat).(le n0 (plus n h1))) (eq_ind_r nat -(plus d2 h2) (\lambda (n0: nat).(le (plus n0 h1) (plus n h1))) (le_S_n (plus -(plus d2 h2) h1) (plus n h1) (lt_le_S (plus (plus d2 h2) h1) (S (plus n h1)) -(le_lt_n_Sm (plus (plus d2 h2) h1) (plus n h1) (plus_le_compat (plus d2 h2) n -h1 h1 H (le_n h1))))) (plus h2 d2) (plus_comm h2 d2)) (plus h2 (plus d2 h1)) -(plus_assoc h2 d2 h1))) (plus d2 h1) (minus_plus h2 (plus d2 h1))))))). - -theorem O_minus: - \forall (x: nat).(\forall (y: nat).((le x y) \to (eq nat (minus x y) O))) -\def - \lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((le n y) \to -(eq nat (minus n y) O)))) (\lambda (y: nat).(\lambda (_: (le O -y)).(refl_equal nat O))) (\lambda (x0: nat).(\lambda (H: ((\forall (y: -nat).((le x0 y) \to (eq nat (minus x0 y) O))))).(\lambda (y: nat).(nat_ind -(\lambda (n: nat).((le (S x0) n) \to (eq nat (match n with [O \Rightarrow (S -x0) | (S l) \Rightarrow (minus x0 l)]) O))) (\lambda (H0: (le (S x0) -O)).(ex2_ind nat (\lambda (n: nat).(eq nat O (S n))) (\lambda (n: nat).(le x0 -n)) (eq nat (S x0) O) (\lambda (x1: nat).(\lambda (H1: (eq nat O (S -x1))).(\lambda (_: (le x0 x1)).(let H3 \def (eq_ind nat O (\lambda (ee: -nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow True -| (S _) \Rightarrow False])) I (S x1) H1) in (False_ind (eq nat (S x0) O) -H3))))) (le_gen_S x0 O H0))) (\lambda (n: nat).(\lambda (_: (((le (S x0) n) -\to (eq nat (match n with [O \Rightarrow (S x0) | (S l) \Rightarrow (minus x0 -l)]) O)))).(\lambda (H1: (le (S x0) (S n))).(H n (le_S_n x0 n H1))))) y)))) -x). - -theorem minus_minus: - \forall (z: nat).(\forall (x: nat).(\forall (y: nat).((le z x) \to ((le z y) -\to ((eq nat (minus x z) (minus y z)) \to (eq nat x y)))))) -\def - \lambda (z: nat).(nat_ind (\lambda (n: nat).(\forall (x: nat).(\forall (y: -nat).((le n x) \to ((le n y) \to ((eq nat (minus x n) (minus y n)) \to (eq -nat x y))))))) (\lambda (x: nat).(\lambda (y: nat).(\lambda (_: (le O -x)).(\lambda (_: (le O y)).(\lambda (H1: (eq nat (minus x O) (minus y -O))).(let H2 \def (eq_ind_r nat (minus x O) (\lambda (n: nat).(eq nat n -(minus y O))) H1 x (minus_n_O x)) in (let H3 \def (eq_ind_r nat (minus y O) -(\lambda (n: nat).(eq nat x n)) H2 y (minus_n_O y)) in H3))))))) (\lambda -(z0: nat).(\lambda (IH: ((\forall (x: nat).(\forall (y: nat).((le z0 x) \to -((le z0 y) \to ((eq nat (minus x z0) (minus y z0)) \to (eq nat x -y)))))))).(\lambda (x: nat).(nat_ind (\lambda (n: nat).(\forall (y: nat).((le -(S z0) n) \to ((le (S z0) y) \to ((eq nat (minus n (S z0)) (minus y (S z0))) -\to (eq nat n y)))))) (\lambda (y: nat).(\lambda (H: (le (S z0) O)).(\lambda -(_: (le (S z0) y)).(\lambda (_: (eq nat (minus O (S z0)) (minus y (S -z0)))).(ex2_ind nat (\lambda (n: nat).(eq nat O (S n))) (\lambda (n: nat).(le -z0 n)) (eq nat O y) (\lambda (x0: nat).(\lambda (H2: (eq nat O (S -x0))).(\lambda (_: (le z0 x0)).(let H4 \def (eq_ind nat O (\lambda (ee: -nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow True -| (S _) \Rightarrow False])) I (S x0) H2) in (False_ind (eq nat O y) H4))))) -(le_gen_S z0 O H)))))) (\lambda (x0: nat).(\lambda (_: ((\forall (y: -nat).((le (S z0) x0) \to ((le (S z0) y) \to ((eq nat (minus x0 (S z0)) (minus -y (S z0))) \to (eq nat x0 y))))))).(\lambda (y: nat).(nat_ind (\lambda (n: -nat).((le (S z0) (S x0)) \to ((le (S z0) n) \to ((eq nat (minus (S x0) (S -z0)) (minus n (S z0))) \to (eq nat (S x0) n))))) (\lambda (_: (le (S z0) (S -x0))).(\lambda (H0: (le (S z0) O)).(\lambda (_: (eq nat (minus (S x0) (S z0)) -(minus O (S z0)))).(ex2_ind nat (\lambda (n: nat).(eq nat O (S n))) (\lambda -(n: nat).(le z0 n)) (eq nat (S x0) O) (\lambda (x1: nat).(\lambda (H2: (eq -nat O (S x1))).(\lambda (_: (le z0 x1)).(let H4 \def (eq_ind nat O (\lambda -(ee: nat).(match ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow -True | (S _) \Rightarrow False])) I (S x1) H2) in (False_ind (eq nat (S x0) -O) H4))))) (le_gen_S z0 O H0))))) (\lambda (y0: nat).(\lambda (_: (((le (S -z0) (S x0)) \to ((le (S z0) y0) \to ((eq nat (minus (S x0) (S z0)) (minus y0 -(S z0))) \to (eq nat (S x0) y0)))))).(\lambda (H: (le (S z0) (S -x0))).(\lambda (H0: (le (S z0) (S y0))).(\lambda (H1: (eq nat (minus (S x0) -(S z0)) (minus (S y0) (S z0)))).(f_equal nat nat S x0 y0 (IH x0 y0 (le_S_n z0 -x0 H) (le_S_n z0 y0 H0) H1))))))) y)))) x)))) z). - -theorem plus_plus: - \forall (z: nat).(\forall (x1: nat).(\forall (x2: nat).(\forall (y1: -nat).(\forall (y2: nat).((le x1 z) \to ((le x2 z) \to ((eq nat (plus (minus z -x1) y1) (plus (minus z x2) y2)) \to (eq nat (plus x1 y2) (plus x2 y1))))))))) -\def - \lambda (z: nat).(nat_ind (\lambda (n: nat).(\forall (x1: nat).(\forall (x2: -nat).(\forall (y1: nat).(\forall (y2: nat).((le x1 n) \to ((le x2 n) \to ((eq -nat (plus (minus n x1) y1) (plus (minus n x2) y2)) \to (eq nat (plus x1 y2) -(plus x2 y1)))))))))) (\lambda (x1: nat).(\lambda (x2: nat).(\lambda (y1: -nat).(\lambda (y2: nat).(\lambda (H: (le x1 O)).(\lambda (H0: (le x2 -O)).(\lambda (H1: (eq nat y1 y2)).(eq_ind nat y1 (\lambda (n: nat).(eq nat -(plus x1 n) (plus x2 y1))) (let H_y \def (le_n_O_eq x2 H0) in (eq_ind nat O -(\lambda (n: nat).(eq nat (plus x1 y1) (plus n y1))) (let H_y0 \def -(le_n_O_eq x1 H) in (eq_ind nat O (\lambda (n: nat).(eq nat (plus n y1) (plus -O y1))) (refl_equal nat (plus O y1)) x1 H_y0)) x2 H_y)) y2 H1)))))))) -(\lambda (z0: nat).(\lambda (IH: ((\forall (x1: nat).(\forall (x2: -nat).(\forall (y1: nat).(\forall (y2: nat).((le x1 z0) \to ((le x2 z0) \to -((eq nat (plus (minus z0 x1) y1) (plus (minus z0 x2) y2)) \to (eq nat (plus -x1 y2) (plus x2 y1))))))))))).(\lambda (x1: nat).(nat_ind (\lambda (n: -nat).(\forall (x2: nat).(\forall (y1: nat).(\forall (y2: nat).((le n (S z0)) -\to ((le x2 (S z0)) \to ((eq nat (plus (minus (S z0) n) y1) (plus (minus (S -z0) x2) y2)) \to (eq nat (plus n y2) (plus x2 y1))))))))) (\lambda (x2: -nat).(nat_ind (\lambda (n: nat).(\forall (y1: nat).(\forall (y2: nat).((le O -(S z0)) \to ((le n (S z0)) \to ((eq nat (plus (minus (S z0) O) y1) (plus -(minus (S z0) n) y2)) \to (eq nat (plus O y2) (plus n y1)))))))) (\lambda -(y1: nat).(\lambda (y2: nat).(\lambda (_: (le O (S z0))).(\lambda (_: (le O -(S z0))).(\lambda (H1: (eq nat (S (plus z0 y1)) (S (plus z0 y2)))).(let H_y -\def (IH O O) in (let H2 \def (eq_ind_r nat (minus z0 O) (\lambda (n: -nat).(\forall (y3: nat).(\forall (y4: nat).((le O z0) \to ((le O z0) \to ((eq -nat (plus n y3) (plus n y4)) \to (eq nat y4 y3))))))) H_y z0 (minus_n_O z0)) -in (H2 y1 y2 (le_O_n z0) (le_O_n z0) (H2 (plus z0 y2) (plus z0 y1) (le_O_n -z0) (le_O_n z0) (f_equal nat nat (plus z0) (plus z0 y2) (plus z0 y1) (sym_eq -nat (plus z0 y1) (plus z0 y2) (eq_add_S (plus z0 y1) (plus z0 y2) -H1)))))))))))) (\lambda (x3: nat).(\lambda (_: ((\forall (y1: nat).(\forall -(y2: nat).((le O (S z0)) \to ((le x3 (S z0)) \to ((eq nat (S (plus z0 y1)) -(plus (match x3 with [O \Rightarrow (S z0) | (S l) \Rightarrow (minus z0 l)]) -y2)) \to (eq nat y2 (plus x3 y1))))))))).(\lambda (y1: nat).(\lambda (y2: -nat).(\lambda (_: (le O (S z0))).(\lambda (H0: (le (S x3) (S z0))).(\lambda -(H1: (eq nat (S (plus z0 y1)) (plus (minus z0 x3) y2))).(let H_y \def (IH O -x3 (S y1)) in (let H2 \def (eq_ind_r nat (minus z0 O) (\lambda (n: -nat).(\forall (y3: nat).((le O z0) \to ((le x3 z0) \to ((eq nat (plus n (S -y1)) (plus (minus z0 x3) y3)) \to (eq nat y3 (plus x3 (S y1)))))))) H_y z0 -(minus_n_O z0)) in (let H3 \def (eq_ind_r nat (plus z0 (S y1)) (\lambda (n: -nat).(\forall (y3: nat).((le O z0) \to ((le x3 z0) \to ((eq nat n (plus -(minus z0 x3) y3)) \to (eq nat y3 (plus x3 (S y1)))))))) H2 (S (plus z0 y1)) -(plus_n_Sm z0 y1)) in (let H4 \def (eq_ind_r nat (plus x3 (S y1)) (\lambda -(n: nat).(\forall (y3: nat).((le O z0) \to ((le x3 z0) \to ((eq nat (S (plus -z0 y1)) (plus (minus z0 x3) y3)) \to (eq nat y3 n)))))) H3 (S (plus x3 y1)) -(plus_n_Sm x3 y1)) in (H4 y2 (le_O_n z0) (le_S_n x3 z0 H0) H1)))))))))))) -x2)) (\lambda (x2: nat).(\lambda (_: ((\forall (x3: nat).(\forall (y1: -nat).(\forall (y2: nat).((le x2 (S z0)) \to ((le x3 (S z0)) \to ((eq nat -(plus (minus (S z0) x2) y1) (plus (minus (S z0) x3) y2)) \to (eq nat (plus x2 -y2) (plus x3 y1)))))))))).(\lambda (x3: nat).(nat_ind (\lambda (n: -nat).(\forall (y1: nat).(\forall (y2: nat).((le (S x2) (S z0)) \to ((le n (S -z0)) \to ((eq nat (plus (minus (S z0) (S x2)) y1) (plus (minus (S z0) n) y2)) -\to (eq nat (plus (S x2) y2) (plus n y1)))))))) (\lambda (y1: nat).(\lambda -(y2: nat).(\lambda (H: (le (S x2) (S z0))).(\lambda (_: (le O (S -z0))).(\lambda (H1: (eq nat (plus (minus z0 x2) y1) (S (plus z0 y2)))).(let -H_y \def (IH x2 O y1 (S y2)) in (let H2 \def (eq_ind_r nat (minus z0 O) -(\lambda (n: nat).((le x2 z0) \to ((le O z0) \to ((eq nat (plus (minus z0 x2) -y1) (plus n (S y2))) \to (eq nat (plus x2 (S y2)) y1))))) H_y z0 (minus_n_O -z0)) in (let H3 \def (eq_ind_r nat (plus z0 (S y2)) (\lambda (n: nat).((le x2 -z0) \to ((le O z0) \to ((eq nat (plus (minus z0 x2) y1) n) \to (eq nat (plus -x2 (S y2)) y1))))) H2 (S (plus z0 y2)) (plus_n_Sm z0 y2)) in (let H4 \def -(eq_ind_r nat (plus x2 (S y2)) (\lambda (n: nat).((le x2 z0) \to ((le O z0) -\to ((eq nat (plus (minus z0 x2) y1) (S (plus z0 y2))) \to (eq nat n y1))))) -H3 (S (plus x2 y2)) (plus_n_Sm x2 y2)) in (H4 (le_S_n x2 z0 H) (le_O_n z0) -H1)))))))))) (\lambda (x4: nat).(\lambda (_: ((\forall (y1: nat).(\forall -(y2: nat).((le (S x2) (S z0)) \to ((le x4 (S z0)) \to ((eq nat (plus (minus -z0 x2) y1) (plus (match x4 with [O \Rightarrow (S z0) | (S l) \Rightarrow -(minus z0 l)]) y2)) \to (eq nat (S (plus x2 y2)) (plus x4 -y1))))))))).(\lambda (y1: nat).(\lambda (y2: nat).(\lambda (H: (le (S x2) (S -z0))).(\lambda (H0: (le (S x4) (S z0))).(\lambda (H1: (eq nat (plus (minus z0 -x2) y1) (plus (minus z0 x4) y2))).(f_equal nat nat S (plus x2 y2) (plus x4 -y1) (IH x2 x4 y1 y2 (le_S_n x2 z0 H) (le_S_n x4 z0 H0) H1))))))))) x3)))) -x1)))) z). - -theorem le_S_minus: - \forall (d: nat).(\forall (h: nat).(\forall (n: nat).((le (plus d h) n) \to -(le d (S (minus n h)))))) -\def - \lambda (d: nat).(\lambda (h: nat).(\lambda (n: nat).(\lambda (H: (le (plus -d h) n)).(let H0 \def (le_trans d (plus d h) n (le_plus_l d h) H) in (let H1 -\def (eq_ind nat n (\lambda (n0: nat).(le d n0)) H0 (plus (minus n h) h) -(le_plus_minus_sym h n (le_trans_plus_r d h n H))) in (le_S d (minus n h) -(le_minus d n h H))))))). - diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/tactics.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/tactics.ma deleted file mode 100644 index 4a7946c68..000000000 --- a/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/tactics.ma +++ /dev/null @@ -1,42 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics". - -include "preamble.ma". - -theorem insert_eq: - \forall (S: Set).(\forall (x: S).(\forall (P: ((S \to Prop))).(\forall (G: -Prop).(((\forall (y: S).((P y) \to ((eq S y x) \to G)))) \to ((P x) \to G))))) -\def - \lambda (S: Set).(\lambda (x: S).(\lambda (P: ((S \to Prop))).(\lambda (G: -Prop).(\lambda (H: ((\forall (y: S).((P y) \to ((eq S y x) \to -G))))).(\lambda (H0: (P x)).(H x H0 (refl_equal S x))))))). - -theorem unintro: - \forall (A: Set).(\forall (a: A).(\forall (P: ((A \to Prop))).(((\forall (x: -A).(P x))) \to (P a)))) -\def - \lambda (A: Set).(\lambda (a: A).(\lambda (P: ((A \to Prop))).(\lambda (H: -((\forall (x: A).(P x)))).(H a)))). - -theorem xinduction: - \forall (A: Set).(\forall (t: A).(\forall (P: ((A \to Prop))).(((\forall (x: -A).((eq A t x) \to (P x)))) \to (P t)))) -\def - \lambda (A: Set).(\lambda (t: A).(\lambda (P: ((A \to Prop))).(\lambda (H: -((\forall (x: A).((eq A t x) \to (P x))))).(H t (refl_equal A t))))). - diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base/plist/defs.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base/plist/defs.ma deleted file mode 100644 index 1ca1142d9..000000000 --- a/matita/contribs/LAMBDA-TYPES/Level-1/Base/plist/defs.ma +++ /dev/null @@ -1,45 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/plist/defs". - -include "preamble.ma". - -inductive PList: Set \def -| PNil: PList -| PCons: nat \to (nat \to (PList \to PList)). - -definition PConsTail: - PList \to (nat \to (nat \to PList)) -\def - let rec PConsTail (hds: PList) on hds: (nat \to (nat \to PList)) \def -(\lambda (h0: nat).(\lambda (d0: nat).(match hds with [PNil \Rightarrow -(PCons h0 d0 PNil) | (PCons h d hds0) \Rightarrow (PCons h d (PConsTail hds0 -h0 d0))]))) in PConsTail. - -definition Ss: - PList \to PList -\def - let rec Ss (hds: PList) on hds: PList \def (match hds with [PNil \Rightarrow -PNil | (PCons h d hds0) \Rightarrow (PCons h (S d) (Ss hds0))]) in Ss. - -definition papp: - PList \to (PList \to PList) -\def - let rec papp (a: PList) on a: (PList \to PList) \def (\lambda (b: -PList).(match a with [PNil \Rightarrow b | (PCons h d a0) \Rightarrow (PCons -h d (papp a0 b))])) in papp. - diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base/plist/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base/plist/props.ma deleted file mode 100644 index 7338262f1..000000000 --- a/matita/contribs/LAMBDA-TYPES/Level-1/Base/plist/props.ma +++ /dev/null @@ -1,33 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/plist/props". - -include "plist/defs.ma". - -theorem papp_ss: - \forall (is1: PList).(\forall (is2: PList).(eq PList (papp (Ss is1) (Ss -is2)) (Ss (papp is1 is2)))) -\def - \lambda (is1: PList).(PList_ind (\lambda (p: PList).(\forall (is2: -PList).(eq PList (papp (Ss p) (Ss is2)) (Ss (papp p is2))))) (\lambda (is2: -PList).(refl_equal PList (Ss is2))) (\lambda (n: nat).(\lambda (n0: -nat).(\lambda (p: PList).(\lambda (H: ((\forall (is2: PList).(eq PList (papp -(Ss p) (Ss is2)) (Ss (papp p is2)))))).(\lambda (is2: PList).(eq_ind_r PList -(Ss (papp p is2)) (\lambda (p0: PList).(eq PList (PCons n (S n0) p0) (PCons n -(S n0) (Ss (papp p is2))))) (refl_equal PList (PCons n (S n0) (Ss (papp p -is2)))) (papp (Ss p) (Ss is2)) (H is2))))))) is1). - diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base/preamble.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base/preamble.ma deleted file mode 100644 index 9b2d974f4..000000000 --- a/matita/contribs/LAMBDA-TYPES/Level-1/Base/preamble.ma +++ /dev/null @@ -1,160 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/preamble". - -include' "../../../../legacy/coq.ma". - -(* FG: This is because "and" is a reserved keyword of the parser *) -alias id "land" = "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)". - -(* FG/CSC: These aliases should disappear: we would like to write something - * like: "disambiguate in cic:/Coq/*" - *) -alias symbol "plus" = "Coq's natural plus". -alias symbol "leq" = "Coq's natural 'less or equal to'". -alias symbol "neq" = "Coq's not equal to (leibnitz)". -alias symbol "eq" = "Coq's leibnitz's equality". - -alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)". -alias id "conj" = "cic:/Coq/Init/Logic/and.ind#xpointer(1/1/1)". -alias id "eq_add_S" = "cic:/Coq/Init/Peano/eq_add_S.con". -alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)". -alias id "eq_ind" = "cic:/Coq/Init/Logic/eq_ind.con". -alias id "eq_ind_r" = "cic:/Coq/Init/Logic/eq_ind_r.con". -alias id "ex2" = "cic:/Coq/Init/Logic/ex2.ind#xpointer(1/1)". -alias id "ex2_ind" = "cic:/Coq/Init/Logic/ex2_ind.con". -alias id "ex" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)". -alias id "ex_intro2" = "cic:/Coq/Init/Logic/ex2.ind#xpointer(1/1/1)". -alias id "false" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1/2)". -alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)". -alias id "False_ind" = "cic:/Coq/Init/Logic/False_ind.con". -alias id "I" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1/1)". -alias id "le_antisym" = "cic:/Coq/Arith/Le/le_antisym.con". -alias id "le" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)". -alias id "le_lt_n_Sm" = "cic:/Coq/Arith/Lt/le_lt_n_Sm.con". -alias id "le_lt_or_eq" = "cic:/Coq/Arith/Lt/le_lt_or_eq.con". -alias id "le_n" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1/1)". -alias id "le_n_O_eq" = "cic:/Coq/Arith/Le/le_n_O_eq.con". -alias id "le_not_lt" = "cic:/Coq/Arith/Lt/le_not_lt.con". -alias id "le_n_S" = "cic:/Coq/Arith/Le/le_n_S.con". -alias id "le_O_n" = "cic:/Coq/Arith/Le/le_O_n.con". -alias id "le_or_lt" = "cic:/Coq/Arith/Lt/le_or_lt.con". -alias id "le_plus_l" = "cic:/Coq/Arith/Plus/le_plus_l.con". -alias id "le_plus_minus" = "cic:/Coq/Arith/Minus/le_plus_minus.con". -alias id "le_plus_minus_r" = "cic:/Coq/Arith/Minus/le_plus_minus_r.con". -alias id "le_plus_r" = "cic:/Coq/Arith/Plus/le_plus_r.con". -alias id "le_S" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1/2)". -alias id "le_S_n" = "cic:/Coq/Arith/Le/le_S_n.con". -alias id "le_Sn_n" = "cic:/Coq/Arith/Le/le_Sn_n.con". -alias id "le_trans" = "cic:/Coq/Arith/Le/le_trans.con". -alias id "lt" = "cic:/Coq/Init/Peano/lt.con". -alias id "lt_irrefl" = "cic:/Coq/Arith/Lt/lt_irrefl.con". -alias id "lt_le_S" = "cic:/Coq/Arith/Lt/lt_le_S.con". -alias id "lt_n_S" = "cic:/Coq/Arith/Lt/lt_n_S.con". -alias id "minus" = "cic:/Coq/Init/Peano/minus.con". -alias id "minus_n_O" = "cic:/Coq/Arith/Minus/minus_n_O.con". -alias id "minus_plus" = "cic:/Coq/Arith/Minus/minus_plus.con". -alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". -alias id "nat_ind" = "cic:/Coq/Init/Datatypes/nat_ind.con". -alias id "not" = "cic:/Coq/Init/Logic/not.con". -alias id "not_eq_S" = "cic:/Coq/Init/Peano/not_eq_S.con". -alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". -alias id "or" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)". -alias id "or_ind" = "cic:/Coq/Init/Logic/or_ind.con". -alias id "or_introl" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1/1)". -alias id "or_intror" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1/2)". -alias id "O_S" = "cic:/Coq/Init/Peano/O_S.con". -alias id "plus_assoc" = "cic:/Coq/Arith/Plus/plus_assoc.con". -alias id "plus_assoc_reverse" = "cic:/Coq/Arith/Plus/plus_assoc_reverse.con". -alias id "plus" = "cic:/Coq/Init/Peano/plus.con". -alias id "plus_comm" = "cic:/Coq/Arith/Plus/plus_comm.con". -alias id "plus_le_compat" = "cic:/Coq/Arith/Plus/plus_le_compat.con". -alias id "plus_le_reg_l" = "cic:/Coq/Arith/Plus/plus_le_reg_l.con". -alias id "plus_lt_reg_l" = "cic:/Coq/Arith/Plus/plus_lt_reg_l.con". -alias id "plus_n_Sm" = "cic:/Coq/Init/Peano/plus_n_Sm.con". -alias id "plus_reg_l" = "cic:/Coq/Arith/Plus/plus_reg_l.con". -alias id "pred" = "cic:/Coq/Init/Peano/pred.con". -alias id "refl_equal" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)". -alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". -alias id "true" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1/1)". -alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". -alias id "plus_lt_compat_r" = "cic:/Coq/Arith/Plus/plus_lt_compat_r.con". -alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con". -alias id "plus_le_lt_compat" = "cic:/Coq/Arith/Plus/plus_le_lt_compat.con". -alias id "lt_wf_ind" = "cic:/Coq/Arith/Wf_nat/lt_wf_ind.con". -alias id "minus_Sn_m" = "cic:/Coq/Arith/Minus/minus_Sn_m.con". -alias id "and_ind" = "cic:/Coq/Init/Logic/and_ind.con". -alias id "le_lt_trans" = "cic:/Coq/Arith/Lt/le_lt_trans.con". -alias id "lt_le_trans" = "cic:/Coq/Arith/Lt/lt_le_trans.con". -alias id "le_lt_trans" = "cic:/Coq/Arith/Lt/le_lt_trans.con". -alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con". -alias id "f_equal3" = "cic:/Coq/Init/Logic/f_equal3.con". -alias id "S_pred" = "cic:/Coq/Arith/Lt/S_pred.con". -alias id "lt_le_trans" = "cic:/Coq/Arith/Lt/lt_le_trans.con". -alias id "plus_lt_compat_r" = "cic:/Coq/Arith/Plus/plus_lt_compat_r.con". -alias id "le_plus_trans" = "cic:/Coq/Arith/Plus/le_plus_trans.con". -alias id "f_equal2" = "cic:/Coq/Init/Logic/f_equal2.con". -alias id "le_plus_trans" = "cic:/Coq/Arith/Plus/le_plus_trans.con". -alias id "f_equal2" = "cic:/Coq/Init/Logic/f_equal2.con". -alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con". -alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con". -alias id "lt_trans" = "cic:/Coq/Arith/Lt/lt_trans.con". -alias id "minus_Sn_m" = "cic:/Coq/Arith/Minus/minus_Sn_m.con". -alias id "ex_intro" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1/1)". -alias id "lt_trans" = "cic:/Coq/Arith/Lt/lt_trans.con". -alias id "lt_n_Sn" = "cic:/Coq/Arith/Lt/lt_n_Sn.con". -alias id "lt_le_trans" = "cic:/Coq/Arith/Lt/lt_le_trans.con". -alias id "lt_wf_ind" = "cic:/Coq/Arith/Wf_nat/lt_wf_ind.con". -alias id "bool_ind" = "cic:/Coq/Init/Datatypes/bool_ind.con". -alias id "ex_ind" = "cic:/Coq/Init/Logic/ex_ind.con". -alias id "plus_Snm_nSm" = "cic:/Coq/Arith/Plus/plus_Snm_nSm.con". -alias id "plus_lt_le_compat" = "cic:/Coq/Arith/Plus/plus_lt_le_compat.con". -alias id "plus_lt_compat" = "cic:/Coq/Arith/Plus/plus_lt_compat.con". -alias id "lt_S_n" = "cic:/Coq/Arith/Lt/lt_S_n.con". -alias id "minus_n_n" = "cic:/Coq/Arith/Minus/minus_n_n.con". - -theorem f_equal: \forall A,B:Type. \forall f:A \to B. - \forall x,y:A. x = y \to f x = f y. - intros. elim H. reflexivity. -qed. - -theorem sym_eq: \forall A:Type. \forall x,y:A. x = y \to y = x. - intros. rewrite > H. reflexivity. -qed. - -theorem sym_not_eq: \forall A:Type. \forall x,y:A. x \neq y \to y \neq x. - unfold not. intros. apply H. symmetry. assumption. -qed. - -theorem trans_eq : \forall A:Type. \forall x,y,z:A. x=y \to y=z \to x=z. - intros. transitivity y; assumption. -qed. - -theorem plus_reg_l: \forall n,m,p. n + m = n + p \to m = p. - intros. apply plus_reg_l; auto. -qed. - -theorem plus_le_reg_l: \forall p,n,m. p + n <= p + m \to n <= m. - intros. apply plus_le_reg_l; auto. -qed. - -default "equality" - cic:/Coq/Init/Logic/eq.ind - cic:/matita/LAMBDA-TYPES/Base-1/preamble/sym_eq.con - cic:/matita/LAMBDA-TYPES/Base-1/preamble/trans_eq.con - cic:/Coq/Init/Logic/eq_ind.con - cic:/Coq/Init/Logic/eq_ind_r.con - cic:/matita/LAMBDA-TYPES/Base-1/preamble/f_equal.con - cic:/matita/legacy/coq/f_equal1.con. diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base/spare.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base/spare.ma deleted file mode 100644 index f66934f78..000000000 --- a/matita/contribs/LAMBDA-TYPES/Level-1/Base/spare.ma +++ /dev/null @@ -1,20 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/spare". - -include "theory.ma". - diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base/theory.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base/theory.ma deleted file mode 100644 index d89a21858..000000000 --- a/matita/contribs/LAMBDA-TYPES/Level-1/Base/theory.ma +++ /dev/null @@ -1,28 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/theory". - -include "ext/tactics.ma". - -include "ext/arith.ma". - -include "types/props.ma". - -include "blt/props.ma". - -include "plist/props.ma". - diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base/types/defs.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base/types/defs.ma deleted file mode 100644 index a60c1ad64..000000000 --- a/matita/contribs/LAMBDA-TYPES/Level-1/Base/types/defs.ma +++ /dev/null @@ -1,150 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/types/defs". - -include "preamble.ma". - -inductive and3 (P0: Prop) (P1: Prop) (P2: Prop): Prop \def -| and3_intro: P0 \to (P1 \to (P2 \to (and3 P0 P1 P2))). - -inductive or3 (P0: Prop) (P1: Prop) (P2: Prop): Prop \def -| or3_intro0: P0 \to (or3 P0 P1 P2) -| or3_intro1: P1 \to (or3 P0 P1 P2) -| or3_intro2: P2 \to (or3 P0 P1 P2). - -inductive or4 (P0: Prop) (P1: Prop) (P2: Prop) (P3: Prop): Prop \def -| or4_intro0: P0 \to (or4 P0 P1 P2 P3) -| or4_intro1: P1 \to (or4 P0 P1 P2 P3) -| or4_intro2: P2 \to (or4 P0 P1 P2 P3) -| or4_intro3: P3 \to (or4 P0 P1 P2 P3). - -inductive ex3 (A0: Set) (P0: A0 \to Prop) (P1: A0 \to Prop) (P2: A0 \to -Prop): Prop \def -| ex3_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to (ex3 A0 -P0 P1 P2)))). - -inductive ex4 (A0: Set) (P0: A0 \to Prop) (P1: A0 \to Prop) (P2: A0 \to Prop) -(P3: A0 \to Prop): Prop \def -| ex4_intro: \forall (x0: A0).((P0 x0) \to ((P1 x0) \to ((P2 x0) \to ((P3 x0) -\to (ex4 A0 P0 P1 P2 P3))))). - -inductive ex_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)): Prop \def -| ex_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to (ex_2 A0 A1 -P0))). - -inductive ex2_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)) (P1: A0 \to -(A1 \to Prop)): Prop \def -| ex2_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1) -\to (ex2_2 A0 A1 P0 P1)))). - -inductive ex3_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)) (P1: A0 \to -(A1 \to Prop)) (P2: A0 \to (A1 \to Prop)): Prop \def -| ex3_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1) -\to ((P2 x0 x1) \to (ex3_2 A0 A1 P0 P1 P2))))). - -inductive ex4_2 (A0: Set) (A1: Set) (P0: A0 \to (A1 \to Prop)) (P1: A0 \to -(A1 \to Prop)) (P2: A0 \to (A1 \to Prop)) (P3: A0 \to (A1 \to Prop)): Prop -\def -| ex4_2_intro: \forall (x0: A0).(\forall (x1: A1).((P0 x0 x1) \to ((P1 x0 x1) -\to ((P2 x0 x1) \to ((P3 x0 x1) \to (ex4_2 A0 A1 P0 P1 P2 P3)))))). - -inductive ex_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to -Prop))): Prop \def -| ex_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 x1 -x2) \to (ex_3 A0 A1 A2 P0)))). - -inductive ex2_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to -Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))): Prop \def -| ex2_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 -x1 x2) \to ((P1 x0 x1 x2) \to (ex2_3 A0 A1 A2 P0 P1))))). - -inductive ex3_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to -Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2 \to -Prop))): Prop \def -| ex3_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 -x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to (ex3_3 A0 A1 A2 P0 P1 -P2)))))). - -inductive ex4_3 (A0: Set) (A1: Set) (A2: Set) (P0: A0 \to (A1 \to (A2 \to -Prop))) (P1: A0 \to (A1 \to (A2 \to Prop))) (P2: A0 \to (A1 \to (A2 \to -Prop))) (P3: A0 \to (A1 \to (A2 \to Prop))): Prop \def -| ex4_3_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).((P0 x0 -x1 x2) \to ((P1 x0 x1 x2) \to ((P2 x0 x1 x2) \to ((P3 x0 x1 x2) \to (ex4_3 A0 -A1 A2 P0 P1 P2 P3))))))). - -inductive ex3_4 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (P0: A0 \to (A1 \to -(A2 \to (A3 \to Prop)))) (P1: A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P2: A0 -\to (A1 \to (A2 \to (A3 \to Prop)))): Prop \def -| ex3_4_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall -(x3: A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to -(ex3_4 A0 A1 A2 A3 P0 P1 P2))))))). - -inductive ex4_4 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (P0: A0 \to (A1 \to -(A2 \to (A3 \to Prop)))) (P1: A0 \to (A1 \to (A2 \to (A3 \to Prop)))) (P2: A0 -\to (A1 \to (A2 \to (A3 \to Prop)))) (P3: A0 \to (A1 \to (A2 \to (A3 \to -Prop)))): Prop \def -| ex4_4_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall -(x3: A3).((P0 x0 x1 x2 x3) \to ((P1 x0 x1 x2 x3) \to ((P2 x0 x1 x2 x3) \to -((P3 x0 x1 x2 x3) \to (ex4_4 A0 A1 A2 A3 P0 P1 P2 P3)))))))). - -inductive ex4_5 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (P0: A0 \to -(A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to -(A4 \to Prop))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P3: -A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))): Prop \def -| ex4_5_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall -(x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0 x1 x2 x3 x4) \to -((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to (ex4_5 A0 A1 A2 A3 A4 P0 P1 -P2 P3))))))))). - -inductive ex5_5 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (P0: A0 \to -(A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to -(A4 \to Prop))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P3: -A0 \to (A1 \to (A2 \to (A3 \to (A4 \to Prop))))) (P4: A0 \to (A1 \to (A2 \to -(A3 \to (A4 \to Prop))))): Prop \def -| ex5_5_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall -(x3: A3).(\forall (x4: A4).((P0 x0 x1 x2 x3 x4) \to ((P1 x0 x1 x2 x3 x4) \to -((P2 x0 x1 x2 x3 x4) \to ((P3 x0 x1 x2 x3 x4) \to ((P4 x0 x1 x2 x3 x4) \to -(ex5_5 A0 A1 A2 A3 A4 P0 P1 P2 P3 P4)))))))))). - -inductive ex6_6 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (A5: Set) -(P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P1: A0 \to -(A1 \to (A2 \to (A3 \to (A4 \to (A5 \to Prop)))))) (P2: A0 \to (A1 \to (A2 -\to (A3 \to (A4 \to (A5 \to Prop)))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to -(A4 \to (A5 \to Prop)))))) (P4: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 -\to Prop)))))) (P5: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to -Prop)))))): Prop \def -| ex6_6_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall -(x3: A3).(\forall (x4: A4).(\forall (x5: A5).((P0 x0 x1 x2 x3 x4 x5) \to ((P1 -x0 x1 x2 x3 x4 x5) \to ((P2 x0 x1 x2 x3 x4 x5) \to ((P3 x0 x1 x2 x3 x4 x5) -\to ((P4 x0 x1 x2 x3 x4 x5) \to ((P5 x0 x1 x2 x3 x4 x5) \to (ex6_6 A0 A1 A2 -A3 A4 A5 P0 P1 P2 P3 P4 P5)))))))))))). - -inductive ex6_7 (A0: Set) (A1: Set) (A2: Set) (A3: Set) (A4: Set) (A5: Set) -(A6: Set) (P0: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to -Prop))))))) (P1: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to -Prop))))))) (P2: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to -Prop))))))) (P3: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to -Prop))))))) (P4: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to -Prop))))))) (P5: A0 \to (A1 \to (A2 \to (A3 \to (A4 \to (A5 \to (A6 \to -Prop))))))): Prop \def -| ex6_7_intro: \forall (x0: A0).(\forall (x1: A1).(\forall (x2: A2).(\forall -(x3: A3).(\forall (x4: A4).(\forall (x5: A5).(\forall (x6: A6).((P0 x0 x1 x2 -x3 x4 x5 x6) \to ((P1 x0 x1 x2 x3 x4 x5 x6) \to ((P2 x0 x1 x2 x3 x4 x5 x6) -\to ((P3 x0 x1 x2 x3 x4 x5 x6) \to ((P4 x0 x1 x2 x3 x4 x5 x6) \to ((P5 x0 x1 -x2 x3 x4 x5 x6) \to (ex6_7 A0 A1 A2 A3 A4 A5 A6 P0 P1 P2 P3 P4 -P5))))))))))))). - diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base/types/props.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base/types/props.ma deleted file mode 100644 index 1c9b499bb..000000000 --- a/matita/contribs/LAMBDA-TYPES/Level-1/Base/types/props.ma +++ /dev/null @@ -1,32 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/types/props". - -include "types/defs.ma". - -theorem ex2_sym: - \forall (A: Set).(\forall (P: ((A \to Prop))).(\forall (Q: ((A \to -Prop))).((ex2 A (\lambda (x: A).(P x)) (\lambda (x: A).(Q x))) \to (ex2 A -(\lambda (x: A).(Q x)) (\lambda (x: A).(P x)))))) -\def - \lambda (A: Set).(\lambda (P: ((A \to Prop))).(\lambda (Q: ((A \to -Prop))).(\lambda (H: (ex2 A (\lambda (x: A).(P x)) (\lambda (x: A).(Q -x)))).(ex2_ind A (\lambda (x: A).(P x)) (\lambda (x: A).(Q x)) (ex2 A -(\lambda (x: A).(Q x)) (\lambda (x: A).(P x))) (\lambda (x: A).(\lambda (H0: -(P x)).(\lambda (H1: (Q x)).(ex_intro2 A (\lambda (x0: A).(Q x0)) (\lambda -(x0: A).(P x0)) x H1 H0)))) H)))). - diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/makefile b/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/makefile deleted file mode 100644 index db1724d0c..000000000 --- a/matita/contribs/LAMBDA-TYPES/Level-1/LambdaDelta/makefile +++ /dev/null @@ -1,39 +0,0 @@ -H=@ - -RT_BASEDIR=../../../../ -OPTIONS=-bench -MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS) -CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) -MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS) -CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) - -devel:=$(shell basename `pwd`) - -ifneq "$(SRC)" "" - XXX="SRC=$(SRC)" -endif - -all: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel) -clean: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel) -cleanall: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all - -all.opt opt: preall.opt - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel) -clean.opt: preall.opt - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel) -cleanall.opt: preall.opt - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all - -%.mo: preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@ -%.mo.opt: preall.opt - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $@ - -preall: - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel) - -preall.opt: - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) init $(devel) -- 2.39.2