From 711e170c2deaa92289d9d4eb7c0e8aedbe62b5cb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 10 Jan 2008 10:45:04 +0000 Subject: [PATCH] contribs should now compile --- matita/contribs/LAMBDA-TYPES/Base-1/Makefile | 10 + .../contribs/LAMBDA-TYPES/Base-1/blt/defs.ma | 2 +- .../contribs/LAMBDA-TYPES/Base-1/blt/props.ma | 2 +- .../LAMBDA-TYPES/Base-1/definitions.ma | 2 +- matita/contribs/LAMBDA-TYPES/Base-1/depends | 13 + .../contribs/LAMBDA-TYPES/Base-1/ext/arith.ma | 2 +- .../LAMBDA-TYPES/Base-1/ext/tactics.ma | 2 +- matita/contribs/LAMBDA-TYPES/Base-1/makefile | 39 --- .../LAMBDA-TYPES/Base-1/plist/defs.ma | 2 +- .../LAMBDA-TYPES/Base-1/plist/props.ma | 2 +- .../contribs/LAMBDA-TYPES/Base-1/preamble.ma | 4 +- matita/contribs/LAMBDA-TYPES/Base-1/root | 2 + matita/contribs/LAMBDA-TYPES/Base-1/spare.ma | 2 +- matita/contribs/LAMBDA-TYPES/Base-1/theory.ma | 2 +- .../LAMBDA-TYPES/Base-1/types/defs.ma | 2 +- .../LAMBDA-TYPES/Base-1/types/props.ma | 2 +- matita/contribs/LAMBDA-TYPES/Base-2/Makefile | 26 ++ .../Base-2/blt/{defs.mma => defs2.mma} | 3 - .../Base-2/blt/{props.mma => props2.mma} | 4 +- matita/contribs/LAMBDA-TYPES/Base-2/depend | 9 - .../Base-2/ext/{arith.mma => arith2.mma} | 2 - .../Base-2/ext/{tactics.mma => tactics2.mma} | 2 - matita/contribs/LAMBDA-TYPES/Base-2/makefile | 58 ----- .../Base-2/plist/{defs.mma => defs2.mma} | 2 - .../Base-2/plist/{props.mma => props2.mma} | 4 +- .../contribs/LAMBDA-TYPES/Base-2/preamble.ma | 30 --- matita/contribs/LAMBDA-TYPES/Base-2/root | 2 + .../Base-2/{theory.mma => theory2.mma} | 12 +- .../Base-2/types/{defs.mma => defs2.mma} | 2 - .../Base-2/types/{props.mma => props2.mma} | 4 +- .../LAMBDA-TYPES/LambdaDelta-1/A/defs.ma | 4 +- .../LAMBDA-TYPES/LambdaDelta-1/C/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/C/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/G/defs.ma | 4 +- .../LAMBDA-TYPES/LambdaDelta-1/Makefile | 10 + .../LAMBDA-TYPES/LambdaDelta-1/T/dec.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/T/defs.ma | 4 +- .../LAMBDA-TYPES/LambdaDelta-1/T/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/aplus/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/aplus/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/aprem/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/aprem/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/arity/aprem.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/arity/cimp.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/arity/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/arity/lift1.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/arity/pr3.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/arity/props.ma | 2 +- .../LambdaDelta-1/arity/subst0.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/asucc/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/asucc/fwd.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/cimp/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/cimp/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/clear/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/clear/drop.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/clear/fwd.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/clear/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/clen/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/clen/getl.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/cnt/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/cnt/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csuba/arity.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csuba/clear.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csuba/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csuba/drop.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csuba/fwd.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csuba/getl.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csuba/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csubc/arity.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csubc/clear.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csubc/csuba.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csubc/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csubc/drop.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csubc/drop1.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csubc/getl.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csubc/props.ma | 2 +- .../LambdaDelta-1/csubst0/clear.ma | 2 +- .../LambdaDelta-1/csubst0/defs.ma | 2 +- .../LambdaDelta-1/csubst0/drop.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csubst0/fwd.ma | 2 +- .../LambdaDelta-1/csubst0/getl.ma | 2 +- .../LambdaDelta-1/csubst0/props.ma | 2 +- .../LambdaDelta-1/csubst1/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csubst1/fwd.ma | 2 +- .../LambdaDelta-1/csubst1/getl.ma | 2 +- .../LambdaDelta-1/csubst1/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csubt/clear.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csubt/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csubt/drop.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csubt/fwd.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csubt/getl.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csubt/pc3.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csubt/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/csubt/ty3.ma | 2 +- .../{definitions.ma => definitions3.ma} | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/depends | 200 +++++++++++++++ .../LAMBDA-TYPES/LambdaDelta-1/drop/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/drop/fwd.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/drop/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/drop1/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/drop1/getl.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/drop1/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/ex0/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/ex0/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/ex1/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/ex2/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/ex2/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/flt/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/flt/props.ma | 2 +- .../LambdaDelta-1/fsubst0/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/fsubst0/fwd.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/getl/clear.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/getl/dec.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/getl/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/getl/drop.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/getl/flt.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/getl/fwd.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/getl/getl.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/getl/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/iso/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/iso/fwd.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/iso/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/leq/asucc.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/leq/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/leq/fwd.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/leq/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/lift/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/lift/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/lift1/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/lift1/fwd.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/llt/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/llt/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/makefile | 39 --- .../LambdaDelta-1/next_plus/defs.ma | 2 +- .../LambdaDelta-1/next_plus/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/nf2/arity.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/nf2/dec.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/nf2/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/nf2/fwd.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/nf2/iso.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/nf2/lift1.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/nf2/pr3.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pc1/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pc1/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pc3/dec.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pc3/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pc3/fsubst0.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pc3/fwd.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pc3/left.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pc3/nf2.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pc3/pc1.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pc3/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pc3/subst1.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pc3/wcpr0.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr0/dec.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr0/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr0/fwd.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr0/pr0.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr0/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr0/subst1.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr1/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr1/pr1.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr1/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr2/clen.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr2/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr2/fwd.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr2/pr2.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr2/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr2/subst1.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr3/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr3/fwd.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr3/iso.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr3/pr1.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr3/pr3.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr3/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr3/subst1.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/pr3/wcpr0.ma | 2 +- .../{preamble.ma => preamble3.ma} | 4 +- .../LAMBDA-TYPES/LambdaDelta-1/r/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/r/props.ma | 2 +- .../contribs/LAMBDA-TYPES/LambdaDelta-1/root | 2 + .../LAMBDA-TYPES/LambdaDelta-1/s/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/s/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/sc3/arity.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/sc3/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/sc3/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/sn3/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/sn3/fwd.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/sn3/lift1.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/sn3/nf2.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma | 2 +- .../LambdaDelta-1/{spare.ma => spare3.ma} | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/subst0/dec.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/subst0/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/subst0/fwd.ma | 2 +- .../LambdaDelta-1/subst0/props.ma | 2 +- .../LambdaDelta-1/subst0/subst0.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/subst0/tlt.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/subst1/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/subst1/fwd.ma | 2 +- .../LambdaDelta-1/subst1/props.ma | 2 +- .../LambdaDelta-1/subst1/subst1.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/tau0/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/tau0/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/tau1/cnt.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/tau1/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/tau1/props.ma | 2 +- .../LambdaDelta-1/{theory.ma => theory3.ma} | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/tlist/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/tlist/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/tlt/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/tlt/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/ty3/arity.ma | 2 +- .../LambdaDelta-1/ty3/arity_props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/ty3/dec.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/ty3/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/ty3/fwd.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma | 2 +- .../LambdaDelta-1/ty3/pr3_props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/wcpr0/defs.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/wcpr0/fwd.ma | 2 +- .../LAMBDA-TYPES/LambdaDelta-1/wcpr0/getl.ma | 2 +- .../LAMBDA-TYPES/Unified-Sub/Lift/defs.ma | 2 +- .../LAMBDA-TYPES/Unified-Sub/Lift/fun.ma | 2 +- .../LAMBDA-TYPES/Unified-Sub/Lift/inv.ma | 2 +- .../LAMBDA-TYPES/Unified-Sub/Lift/props.ma | 2 +- .../LAMBDA-TYPES/Unified-Sub/Makefile | 10 + .../Unified-Sub/datatypes/Context.ma | 2 +- .../Unified-Sub/datatypes/Term.ma | 4 +- .../contribs/LAMBDA-TYPES/Unified-Sub/depends | 12 + .../LAMBDA-TYPES/Unified-Sub/makefile | 39 --- .../Unified-Sub/{preamble.ma => preamble4.ma} | 10 +- matita/contribs/LAMBDA-TYPES/Unified-Sub/root | 2 + matita/contribs/prova.ma | 236 ------------------ 245 files changed, 525 insertions(+), 705 deletions(-) create mode 100644 matita/contribs/LAMBDA-TYPES/Base-1/Makefile create mode 100644 matita/contribs/LAMBDA-TYPES/Base-1/depends delete mode 100644 matita/contribs/LAMBDA-TYPES/Base-1/makefile create mode 100644 matita/contribs/LAMBDA-TYPES/Base-1/root create mode 100644 matita/contribs/LAMBDA-TYPES/Base-2/Makefile rename matita/contribs/LAMBDA-TYPES/Base-2/blt/{defs.mma => defs2.mma} (94%) rename matita/contribs/LAMBDA-TYPES/Base-2/blt/{props.mma => props2.mma} (94%) delete mode 100644 matita/contribs/LAMBDA-TYPES/Base-2/depend rename matita/contribs/LAMBDA-TYPES/Base-2/ext/{arith.mma => arith2.mma} (98%) rename matita/contribs/LAMBDA-TYPES/Base-2/ext/{tactics.mma => tactics2.mma} (95%) delete mode 100644 matita/contribs/LAMBDA-TYPES/Base-2/makefile rename matita/contribs/LAMBDA-TYPES/Base-2/plist/{defs.mma => defs2.mma} (95%) rename matita/contribs/LAMBDA-TYPES/Base-2/plist/{props.mma => props2.mma} (93%) delete mode 100644 matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma create mode 100644 matita/contribs/LAMBDA-TYPES/Base-2/root rename matita/contribs/LAMBDA-TYPES/Base-2/{theory.mma => theory2.mma} (85%) rename matita/contribs/LAMBDA-TYPES/Base-2/types/{defs.mma => defs2.mma} (96%) rename matita/contribs/LAMBDA-TYPES/Base-2/types/{props.mma => props2.mma} (93%) create mode 100644 matita/contribs/LAMBDA-TYPES/LambdaDelta-1/Makefile rename matita/contribs/LAMBDA-TYPES/LambdaDelta-1/{definitions.ma => definitions3.ma} (96%) create mode 100644 matita/contribs/LAMBDA-TYPES/LambdaDelta-1/depends delete mode 100644 matita/contribs/LAMBDA-TYPES/LambdaDelta-1/makefile rename matita/contribs/LAMBDA-TYPES/LambdaDelta-1/{preamble.ma => preamble3.ma} (96%) create mode 100644 matita/contribs/LAMBDA-TYPES/LambdaDelta-1/root rename matita/contribs/LAMBDA-TYPES/LambdaDelta-1/{spare.ma => spare3.ma} (99%) rename matita/contribs/LAMBDA-TYPES/LambdaDelta-1/{theory.ma => theory3.ma} (95%) create mode 100644 matita/contribs/LAMBDA-TYPES/Unified-Sub/Makefile create mode 100644 matita/contribs/LAMBDA-TYPES/Unified-Sub/depends delete mode 100644 matita/contribs/LAMBDA-TYPES/Unified-Sub/makefile rename matita/contribs/LAMBDA-TYPES/Unified-Sub/{preamble.ma => preamble4.ma} (85%) create mode 100644 matita/contribs/LAMBDA-TYPES/Unified-Sub/root delete mode 100644 matita/contribs/prova.ma diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/Makefile b/matita/contribs/LAMBDA-TYPES/Base-1/Makefile new file mode 100644 index 000000000..29cae5c9b --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-1/Makefile @@ -0,0 +1,10 @@ +DIR=$(shell basename $$PWD) + +$(DIR) all: + ../../../matitac +$(DIR).opt opt all.opt: + ../../../matitac.opt +clean: + ../../../matitaclean +clean.opt: + ../../../matitaclean.opt diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/blt/defs.ma b/matita/contribs/LAMBDA-TYPES/Base-1/blt/defs.ma index 4864a2c86..a7dbfcbd6 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-1/blt/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/Base-1/blt/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/blt/defs". + include "preamble.ma". diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/blt/props.ma b/matita/contribs/LAMBDA-TYPES/Base-1/blt/props.ma index c7952ebd2..0f735ac5f 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-1/blt/props.ma +++ b/matita/contribs/LAMBDA-TYPES/Base-1/blt/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/blt/props". + include "blt/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/definitions.ma b/matita/contribs/LAMBDA-TYPES/Base-1/definitions.ma index ec3212d25..240efefe0 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-1/definitions.ma +++ b/matita/contribs/LAMBDA-TYPES/Base-1/definitions.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/definitions". + include "types/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/depends b/matita/contribs/LAMBDA-TYPES/Base-1/depends new file mode 100644 index 000000000..9bb223d98 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-1/depends @@ -0,0 +1,13 @@ +definitions.ma blt/defs.ma plist/defs.ma types/defs.ma +preamble.ma coq.ma +theory.ma blt/props.ma ext/arith.ma ext/tactics.ma plist/props.ma types/props.ma +spare.ma theory.ma +plist/props.ma plist/defs.ma +plist/defs.ma preamble.ma +ext/tactics.ma preamble.ma +ext/arith.ma preamble.ma +types/props.ma types/defs.ma +types/defs.ma preamble.ma +blt/props.ma blt/defs.ma +blt/defs.ma preamble.ma +coq.ma diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma b/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma index e8a076513..95d322b55 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma +++ b/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith". + include "preamble.ma". diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/ext/tactics.ma b/matita/contribs/LAMBDA-TYPES/Base-1/ext/tactics.ma index 4a7946c68..c23428942 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-1/ext/tactics.ma +++ b/matita/contribs/LAMBDA-TYPES/Base-1/ext/tactics.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics". + include "preamble.ma". diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/makefile b/matita/contribs/LAMBDA-TYPES/Base-1/makefile deleted file mode 100644 index 3198e94cf..000000000 --- a/matita/contribs/LAMBDA-TYPES/Base-1/makefile +++ /dev/null @@ -1,39 +0,0 @@ -H= @ - -RT_BASEDIR=../../../ -OPTIONS=-bench -onepass -system -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) $(@:.opt=) - -preall: - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel) - -preall.opt: - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) init $(devel) diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/plist/defs.ma b/matita/contribs/LAMBDA-TYPES/Base-1/plist/defs.ma index 1ca1142d9..71cbd156a 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-1/plist/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/Base-1/plist/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/plist/defs". + include "preamble.ma". diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/plist/props.ma b/matita/contribs/LAMBDA-TYPES/Base-1/plist/props.ma index 7338262f1..d40a3a887 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-1/plist/props.ma +++ b/matita/contribs/LAMBDA-TYPES/Base-1/plist/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/plist/props". + include "plist/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma b/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma index f5ad380c9..29ebdfeff 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma +++ b/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/preamble". -include' "../../../legacy/coq.ma". + +include "coq.ma". alias symbol "eq" = "Coq's leibnitz's equality". alias symbol "leq" = "Coq's natural 'less or equal to'". diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/root b/matita/contribs/LAMBDA-TYPES/Base-1/root new file mode 100644 index 000000000..43a60f943 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-1/root @@ -0,0 +1,2 @@ +baseuri=cic:/matita/LAMBDA-TYPES/Base-1 +include_paths= ../../../legacy diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/spare.ma b/matita/contribs/LAMBDA-TYPES/Base-1/spare.ma index e19f961cc..fbcaab295 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-1/spare.ma +++ b/matita/contribs/LAMBDA-TYPES/Base-1/spare.ma @@ -14,7 +14,7 @@ (* 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/Base-1/theory.ma b/matita/contribs/LAMBDA-TYPES/Base-1/theory.ma index d89a21858..9aae1717a 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-1/theory.ma +++ b/matita/contribs/LAMBDA-TYPES/Base-1/theory.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/theory". + include "ext/tactics.ma". diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma b/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma index 638fd2e49..0f0b999ad 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/types/defs". + include "preamble.ma". diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/types/props.ma b/matita/contribs/LAMBDA-TYPES/Base-1/types/props.ma index 1c9b499bb..6917ec13d 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-1/types/props.ma +++ b/matita/contribs/LAMBDA-TYPES/Base-1/types/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/types/props". + include "types/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/Makefile b/matita/contribs/LAMBDA-TYPES/Base-2/Makefile new file mode 100644 index 000000000..f67b79581 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/Makefile @@ -0,0 +1,26 @@ +DIR=$(shell basename $$PWD) + +MMAS = $(shell find -name "*.mma") +MAS = $(MMAS:%.mma=%.ma) + +%.ma: %.mma + echo -e "$< preamble.ma \npreamble.ma" > depends + ../../../matitac.opt -dump $@ $< 2>/dev/null + ../../../matitadep.opt + ../../../matitac.opt $@ + +$(DIR) all: $(MAS) + ../../../matitac +$(DIR).opt opt all.opt: $(MAS) + ../../../matitac.opt +clean: + ../../../matitaclean + rm -f $(MAS) +clean.opt: + ../../../matitaclean.opt + rm -f $(MAS) + +theory2.ma: theory2.mma ext/tactics2.ma ext/arith2.ma types/props2.ma blt/props2.ma plist/props2.ma +types/props2.ma: types/props2.mma types/defs2.ma +blt/props2.ma: blt/props2.mma blt/defs2.ma +plist/props2.ma: plist/props2.mma plist/defs2.ma diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs.mma b/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs2.mma similarity index 94% rename from matita/contribs/LAMBDA-TYPES/Base-2/blt/defs.mma rename to matita/contribs/LAMBDA-TYPES/Base-2/blt/defs2.mma index 12438b398..6eb948342 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs.mma +++ b/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs2.mma @@ -14,10 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/blt/defs". - include "preamble.ma". - (* object blt not inlined *) diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/blt/props.mma b/matita/contribs/LAMBDA-TYPES/Base-2/blt/props2.mma similarity index 94% rename from matita/contribs/LAMBDA-TYPES/Base-2/blt/props.mma rename to matita/contribs/LAMBDA-TYPES/Base-2/blt/props2.mma index d24466394..1fd2047fd 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-2/blt/props.mma +++ b/matita/contribs/LAMBDA-TYPES/Base-2/blt/props2.mma @@ -14,9 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/blt/props". - -include "blt/defs.ma". +include "blt/defs2.ma". inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/lt_blt.con". diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/depend b/matita/contribs/LAMBDA-TYPES/Base-2/depend deleted file mode 100644 index 4ac4a61a6..000000000 --- a/matita/contribs/LAMBDA-TYPES/Base-2/depend +++ /dev/null @@ -1,9 +0,0 @@ -theory.ma: theory.mma ext/tactics.ma ext/arith.ma types/props.ma blt/props.ma plist/props.ma | ext/tactics.mo.opt ext/arith.mo.opt types/props.mo.opt blt/props.mo.opt plist/props.mo.opt -ext/tactics.ma: ext/tactics.mma preamble.ma | preamble.mo.opt -ext/arith.ma: ext/arith.mma preamble.ma | preamble.mo.opt -types/defs.ma: types/defs.mma preamble.ma | preamble.mo.opt -types/props.ma: types/props.mma types/defs.ma | types/defs.mo.opt -blt/defs.ma: blt/defs.mma preamble.ma | preamble.mo.opt -blt/props.ma: blt/props.mma blt/defs.ma | blt/defs.mo.opt -plist/defs.ma: plist/defs.mma preamble.ma | preamble.mo.opt -plist/props.ma: plist/props.mma plist/defs.ma | plist/defs.mo.opt diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith.mma b/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith2.mma similarity index 98% rename from matita/contribs/LAMBDA-TYPES/Base-2/ext/arith.mma rename to matita/contribs/LAMBDA-TYPES/Base-2/ext/arith2.mma index ee4663a51..436b497c9 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith.mma +++ b/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith2.mma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/ext/arith". - include "preamble.ma". inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/nat_dec.con". diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma b/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics2.mma similarity index 95% rename from matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma rename to matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics2.mma index 18de7f71a..e6b75198a 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma +++ b/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics2.mma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/ext/tactics". - include "preamble.ma". inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/insert_eq.con". diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/makefile b/matita/contribs/LAMBDA-TYPES/Base-2/makefile deleted file mode 100644 index f20e608d8..000000000 --- a/matita/contribs/LAMBDA-TYPES/Base-2/makefile +++ /dev/null @@ -1,58 +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: build_mas preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel) -clean: clean_mas preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel) -cleanall: clean_mas preall - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all - -all.opt opt: build_mas preall.opt - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel) -clean.opt: clean_mas preall.opt - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel) -cleanall.opt: clean_mas 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) $(@:.opt=) - -preall: - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel) - -preall.opt: - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) init $(devel) - -# FG: added part ############################################################ - -MATITAC = $(RT_BASEDIR)/matitac.opt - -MMAS = $(shell find -name "*.mma") -MAS = $(MMAS:%.mma=%.ma) - -build_mas: preall.opt $(MAS) - -clean_mas: - $(H)rm -f $(MAS) - -%.ma: %.mma - $(H)$(MATITAC) -dump $@ $< $(OPTIONS) - -include depend - -.DELETE_ON_ERROR: diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs.mma b/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs2.mma similarity index 95% rename from matita/contribs/LAMBDA-TYPES/Base-2/plist/defs.mma rename to matita/contribs/LAMBDA-TYPES/Base-2/plist/defs2.mma index 3dc03da0b..4ae6d5156 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs.mma +++ b/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs2.mma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/plist/defs". - include "preamble.ma". diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma b/matita/contribs/LAMBDA-TYPES/Base-2/plist/props2.mma similarity index 93% rename from matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma rename to matita/contribs/LAMBDA-TYPES/Base-2/plist/props2.mma index 29357a88a..f9cec902e 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma +++ b/matita/contribs/LAMBDA-TYPES/Base-2/plist/props2.mma @@ -14,9 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/plist/props". - -include "plist/defs.ma". +include "plist/defs2.ma". inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/plist/props/papp_ss.con". diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma b/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma deleted file mode 100644 index f04df2037..000000000 --- a/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma +++ /dev/null @@ -1,30 +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-2/preamble". - -include "../Base-1/definitions.ma". - -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:/Coq/Init/Logic/eq_rec.con - cic:/Coq/Init/Logic/eq_rec_r.con - cic:/Coq/Init/Logic/eq_rect.con - cic:/Coq/Init/Logic/eq_rect_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/Base-2/root b/matita/contribs/LAMBDA-TYPES/Base-2/root new file mode 100644 index 000000000..229adbd73 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/root @@ -0,0 +1,2 @@ +baseuri=cic:/matita/LAMBDA-TYPES/Base-2 +include_paths= ../Base-1 ../../../legacy diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/theory.mma b/matita/contribs/LAMBDA-TYPES/Base-2/theory2.mma similarity index 85% rename from matita/contribs/LAMBDA-TYPES/Base-2/theory.mma rename to matita/contribs/LAMBDA-TYPES/Base-2/theory2.mma index 1adab3e2b..d1a0ca8b4 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-2/theory.mma +++ b/matita/contribs/LAMBDA-TYPES/Base-2/theory2.mma @@ -14,15 +14,13 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/theory". +include "ext/tactics2.ma". -include "ext/tactics.ma". +include "ext/arith2.ma". -include "ext/arith.ma". +include "types/props2.ma". -include "types/props.ma". +include "blt/props2.ma". -include "blt/props.ma". - -include "plist/props.ma". +include "plist/props2.ma". diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/types/defs.mma b/matita/contribs/LAMBDA-TYPES/Base-2/types/defs2.mma similarity index 96% rename from matita/contribs/LAMBDA-TYPES/Base-2/types/defs.mma rename to matita/contribs/LAMBDA-TYPES/Base-2/types/defs2.mma index 000f283aa..594edd269 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-2/types/defs.mma +++ b/matita/contribs/LAMBDA-TYPES/Base-2/types/defs2.mma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/types/defs". - include "preamble.ma". diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma b/matita/contribs/LAMBDA-TYPES/Base-2/types/props2.mma similarity index 93% rename from matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma rename to matita/contribs/LAMBDA-TYPES/Base-2/types/props2.mma index d79bfc46b..10b502461 100644 --- a/matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma +++ b/matita/contribs/LAMBDA-TYPES/Base-2/types/props2.mma @@ -14,9 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/types/props". - -include "types/defs.ma". +include "types/defs2.ma". inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/types/props/ex2_sym.con". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/A/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/A/defs.ma index 1c592efd2..b1c263edc 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/A/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/A/defs.ma @@ -14,9 +14,9 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/A/defs". -include "preamble.ma". + +include "preamble3.ma". inductive A: Set \def | ASort: nat \to (nat \to A) diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/defs.ma index 0022395ce..ed683a835 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/C/defs". + include "T/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/props.ma index 30901423e..c983c7864 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/C/props". + include "C/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/G/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/G/defs.ma index d66873d06..10d9d9d54 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/G/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/G/defs.ma @@ -14,9 +14,9 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/G/defs". -include "preamble.ma". + +include "preamble3.ma". record G : Set \def { next: (nat \to nat); diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/Makefile b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/Makefile new file mode 100644 index 000000000..29cae5c9b --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/Makefile @@ -0,0 +1,10 @@ +DIR=$(shell basename $$PWD) + +$(DIR) all: + ../../../matitac +$(DIR).opt opt all.opt: + ../../../matitac.opt +clean: + ../../../matitaclean +clean.opt: + ../../../matitaclean.opt diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/dec.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/dec.ma index 0d05ba97f..18fe43977 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/dec.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/dec.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/dec". + include "T/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/defs.ma index 236063dcf..f98aaf418 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/defs.ma @@ -14,9 +14,9 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs". -include "preamble.ma". + +include "preamble3.ma". inductive B: Set \def | Abbr: B diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/props.ma index 1c661524e..c9b9619f4 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/props". + include "T/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/defs.ma index 0a1c35ea2..9789157aa 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/aplus/defs". + include "asucc/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/props.ma index 16adef5c3..7ea6fb43a 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/aplus/props". + include "aplus/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/defs.ma index 258037275..e8da5937c 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/aprem/defs". + include "A/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/props.ma index 60264bca2..7b8320a9c 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/aprem/props". + include "aprem/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/aprem.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/aprem.ma index e3a36f11c..84bd49b7e 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/aprem.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/aprem.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/aprem". + include "arity/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/cimp.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/cimp.ma index 2af721d15..6e6662c26 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/cimp.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/cimp.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/cimp". + include "arity/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/defs.ma index 410400d5f..38edb49c1 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/defs". + include "leq/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma index fbdcd3848..e2a3e0792 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/fwd". + include "arity/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/lift1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/lift1.ma index 46e4c8c86..cf2844c30 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/lift1.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/lift1.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/lift1". + include "arity/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/pr3.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/pr3.ma index 7b60c2af4..eaedb44aa 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/pr3.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/pr3.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/pr3". + include "csuba/arity.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/props.ma index 6c9662aeb..ec9fdb595 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/props". + include "arity/fwd.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/subst0.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/subst0.ma index 4592f394a..d826c0155 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/subst0.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/subst0.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/subst0". + include "arity/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/defs.ma index ae2233051..eb22b192e 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/asucc/defs". + include "A/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/fwd.ma index d2c77132e..b6f65337a 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/asucc/fwd". + include "asucc/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/defs.ma index c5390f97b..75eb7959b 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/cimp/defs". + include "getl/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/props.ma index ae0f6a567..263d95fd2 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/cimp/props". + include "cimp/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/defs.ma index 118dc7ccf..4fffe08a3 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clear/defs". + include "C/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/drop.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/drop.ma index 2cfcaa874..142bf6ce7 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/drop.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/drop.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clear/drop". + include "clear/fwd.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/fwd.ma index 4749583de..ef2a4d4d9 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clear/fwd". + include "clear/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/props.ma index a1880711d..2d3a7b623 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clear/props". + include "clear/fwd.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/defs.ma index 2885518ea..85679b7fb 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clen/defs". + include "C/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/getl.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/getl.ma index 8773297ca..cd4c81674 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/getl.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/getl.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clen/getl". + include "clen/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/defs.ma index f9b4334e1..946a9c476 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/cnt/defs". + include "T/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/props.ma index 81620ce9e..483834e82 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/cnt/props". + include "cnt/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/arity.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/arity.ma index ff9d01c9e..6b8cf3462 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/arity.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/arity.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/arity". + include "csuba/getl.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/clear.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/clear.ma index 036ca2882..43f490004 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/clear.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/clear.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/clear". + include "csuba/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/defs.ma index 1b8612a2f..a47262249 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/defs". + include "arity/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/drop.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/drop.ma index 003b18a5e..01ed2fb11 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/drop.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/drop.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/drop". + include "csuba/fwd.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/fwd.ma index 2b56bc7a0..0ba50cbbd 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/fwd". + include "csuba/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/getl.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/getl.ma index d93e4d618..5e9baff2c 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/getl.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/getl.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/getl". + include "csuba/drop.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/props.ma index 62e10c095..590a89f2e 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/props". + include "csuba/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/arity.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/arity.ma index d697f1257..b705f618e 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/arity.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/arity.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/arity". + include "csubc/csuba.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/clear.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/clear.ma index 059c359ab..1ddc85ae2 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/clear.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/clear.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/clear". + include "csubc/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/csuba.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/csuba.ma index 646247a79..c4a7269fb 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/csuba.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/csuba.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/csuba". + include "csubc/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/defs.ma index 6348a632b..08943ec39 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/defs". + include "sc3/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop.ma index 301cba935..748c71484 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/drop". + include "csubc/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop1.ma index 75651a172..181f3601e 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop1.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop1.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/drop1". + include "csubc/drop.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/getl.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/getl.ma index dd2a0397c..6bfecf5a3 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/getl.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/getl.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/getl". + include "csubc/drop.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/props.ma index d13d2b09f..ccebb72e8 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/props". + include "csubc/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/clear.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/clear.ma index fb9fdf5a5..2fc335e58 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/clear.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/clear.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/clear". + include "csubst0/fwd.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/defs.ma index 5d90ea599..df56d48aa 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/defs". + include "subst0/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/drop.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/drop.ma index b1a063208..98f094101 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/drop.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/drop.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/drop". + include "csubst0/fwd.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/fwd.ma index 7980be5fc..1b55e2acb 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/fwd". + include "csubst0/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/getl.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/getl.ma index d4ccb6ee5..175c1ae27 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/getl.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/getl.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/getl". + include "csubst0/clear.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/props.ma index 24e20c400..692dbfd87 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/props". + include "csubst0/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/defs.ma index a298dfc8c..f2b0df4c9 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst1/defs". + include "csubst0/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/fwd.ma index 96e86eea5..0f4e479e9 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst1/fwd". + include "csubst1/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/getl.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/getl.ma index a6af74625..8ade743e9 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/getl.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/getl.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst1/getl". + include "csubst1/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/props.ma index 9cafa826f..c9c7528e6 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst1/props". + include "csubst1/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/clear.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/clear.ma index 22581895b..69b533d26 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/clear.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/clear.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/clear". + include "csubt/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/defs.ma index 3f90ff3ce..22ce12082 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/defs". + include "ty3/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/drop.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/drop.ma index 7a7efe4ce..567fcce7d 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/drop.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/drop.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/drop". + include "csubt/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/fwd.ma index 92e19a503..f541ecb34 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/fwd". + include "csubt/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/getl.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/getl.ma index a0f89e0fa..b8da01d6c 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/getl.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/getl.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/getl". + include "csubt/fwd.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/pc3.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/pc3.ma index d8a6ad246..3330b56b2 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/pc3.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/pc3.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/pc3". + include "csubt/getl.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/props.ma index 5d88520a9..115ddda34 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/props". + include "csubt/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3.ma index 3fbcb516f..23677feed 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3". + include "csubt/pc3.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions3.ma similarity index 96% rename from matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions3.ma index 620154782..61d77ed54 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions3.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/definitions". + include "tlt/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/depends b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/depends new file mode 100644 index 000000000..23eb363fd --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/depends @@ -0,0 +1,200 @@ +definitions3.ma aprem/defs.ma cimp/defs.ma clen/defs.ma cnt/defs.ma csuba/defs.ma csubc/defs.ma csubst1/defs.ma csubt/defs.ma ex0/defs.ma ex1/defs.ma ex2/defs.ma flt/defs.ma fsubst0/defs.ma iso/defs.ma llt/defs.ma next_plus/defs.ma nf2/defs.ma pc1/defs.ma subst1/defs.ma tau1/defs.ma tlt/defs.ma wcpr0/defs.ma +preamble3.ma theory.ma +spare.ma theory.ma +theory3.ma ex0/props.ma ex1/props.ma ex2/props.ma pr3/wcpr0.ma subst0/tlt.ma tau1/cnt.ma ty3/dec.ma ty3/nf2.ma ty3/tau0.ma wcpr0/fwd.ma +tlist/props.ma tlist/defs.ma +tlist/defs.ma T/defs.ma +clen/defs.ma C/defs.ma s/defs.ma +clen/getl.ma clen/defs.ma getl/props.ma +leq/props.ma aplus/props.ma leq/defs.ma +leq/asucc.ma aplus/props.ma leq/props.ma +leq/defs.ma aplus/defs.ma +leq/fwd.ma leq/defs.ma +pr3/props.ma pr1/props.ma pr2/props.ma pr3/pr1.ma +pr3/pr3.ma pr2/pr2.ma pr3/props.ma +pr3/defs.ma pr2/defs.ma +pr3/fwd.ma pr2/fwd.ma pr3/props.ma +pr3/subst1.ma pr2/subst1.ma pr3/defs.ma +pr3/iso.ma iso/props.ma pr3/fwd.ma tlist/props.ma +pr3/wcpr0.ma pr3/props.ma wcpr0/getl.ma +pr3/pr1.ma pr1/defs.ma pr3/defs.ma +ty3/fsubst0.ma csubst0/props.ma getl/getl.ma pc3/fsubst0.ma ty3/props.ma +ty3/nf2.ma nf2/arity.ma pc3/nf2.ma ty3/arity.ma +ty3/props.ma pc3/fwd.ma ty3/fwd.ma +ty3/arity_props.ma sc3/arity.ma ty3/arity.ma ty3/fwd.ma +ty3/arity.ma arity/pr3.ma asucc/fwd.ma ty3/pr3_props.ma +ty3/pr3_props.ma ty3/pr3.ma +ty3/tau0.ma tau0/defs.ma ty3/pr3_props.ma +ty3/pr3.ma csubt/ty3.ma pc1/props.ma pc3/pc1.ma pc3/wcpr0.ma ty3/fsubst0.ma ty3/subst1.ma +ty3/defs.ma G/defs.ma pc3/defs.ma +ty3/fwd.ma pc3/props.ma ty3/defs.ma +ty3/dec.ma getl/dec.ma getl/flt.ma pc3/dec.ma ty3/pr3_props.ma +ty3/subst1.ma csubst1/fwd.ma csubst1/getl.ma getl/getl.ma pc3/fwd.ma pc3/subst1.ma ty3/props.ma +cnt/props.ma cnt/defs.ma lift/fwd.ma +cnt/defs.ma T/defs.ma +fsubst0/defs.ma csubst0/defs.ma subst0/defs.ma +fsubst0/fwd.ma fsubst0/defs.ma +iso/props.ma iso/fwd.ma +iso/defs.ma T/defs.ma +iso/fwd.ma iso/defs.ma tlist/defs.ma +lift/props.ma lift/fwd.ma s/props.ma tlist/defs.ma +lift/defs.ma T/defs.ma s/defs.ma tlist/defs.ma +lift/tlt.ma lift/fwd.ma tlt/props.ma +lift/fwd.ma lift/defs.ma +flt/props.ma C/props.ma flt/defs.ma +flt/defs.ma C/defs.ma +A/defs.ma preamble3.ma +subst0/props.ma lift/props.ma subst0/fwd.ma +subst0/defs.ma lift/defs.ma +subst0/tlt.ma lift/props.ma lift/tlt.ma subst0/defs.ma +subst0/fwd.ma lift/props.ma subst0/defs.ma +subst0/subst0.ma subst0/props.ma +subst0/dec.ma lift/props.ma subst0/defs.ma +pr1/props.ma T/props.ma pr0/subst1.ma pr1/defs.ma subst1/props.ma +pr1/defs.ma pr0/defs.ma +pr1/pr1.ma pr0/pr0.ma pr1/props.ma +T/props.ma T/defs.ma +T/defs.ma preamble3.ma +T/dec.ma T/defs.ma +sc3/props.ma arity/aprem.ma arity/lift1.ma csuba/arity.ma drop1/getl.ma drop1/props.ma lift1/props.ma llt/props.ma nf2/lift1.ma sc3/defs.ma sn3/lift1.ma +sc3/arity.ma csubc/arity.ma csubc/drop1.ma csubc/getl.ma csubc/props.ma +sc3/defs.ma arity/defs.ma drop1/defs.ma sn3/defs.ma +tau1/props.ma tau0/props.ma tau1/defs.ma +tau1/defs.ma tau0/defs.ma +tau1/cnt.ma cnt/props.ma tau1/props.ma +aplus/props.ma aplus/defs.ma next_plus/props.ma +aplus/defs.ma asucc/defs.ma +asucc/defs.ma A/defs.ma G/defs.ma +asucc/fwd.ma asucc/defs.ma +aprem/props.ma aprem/defs.ma leq/defs.ma +aprem/defs.ma A/defs.ma +nf2/props.ma nf2/defs.ma pr2/fwd.ma +nf2/arity.ma arity/subst0.ma nf2/fwd.ma +nf2/pr3.ma nf2/defs.ma pr3/pr3.ma +nf2/defs.ma pr2/defs.ma +nf2/fwd.ma T/props.ma nf2/defs.ma pr2/clen.ma subst0/dec.ma +nf2/dec.ma C/props.ma nf2/defs.ma pr0/dec.ma pr2/clen.ma pr2/fwd.ma +nf2/lift1.ma drop1/defs.ma nf2/props.ma +nf2/iso.ma iso/props.ma nf2/pr3.ma pr3/fwd.ma +drop/props.ma drop/fwd.ma lift/props.ma r/props.ma +drop/defs.ma C/defs.ma lift/defs.ma r/defs.ma +drop/fwd.ma drop/defs.ma +csuba/drop.ma csuba/fwd.ma drop/fwd.ma +csuba/clear.ma clear/fwd.ma csuba/defs.ma +csuba/props.ma csuba/defs.ma +csuba/arity.ma T/props.ma arity/props.ma csuba/getl.ma csuba/props.ma +csuba/defs.ma arity/defs.ma +csuba/fwd.ma csuba/defs.ma +csuba/getl.ma csuba/clear.ma csuba/drop.ma getl/clear.ma +C/props.ma C/defs.ma T/props.ma +C/defs.ma T/defs.ma +csubt/drop.ma csubt/defs.ma drop/fwd.ma +csubt/clear.ma clear/fwd.ma csubt/defs.ma +csubt/props.ma csubt/defs.ma +csubt/pc3.ma csubt/getl.ma pc3/left.ma +csubt/defs.ma ty3/defs.ma +csubt/fwd.ma csubt/defs.ma +csubt/ty3.ma csubt/pc3.ma csubt/props.ma +csubt/getl.ma csubt/clear.ma csubt/drop.ma csubt/fwd.ma getl/clear.ma +cimp/props.ma cimp/defs.ma getl/getl.ma +cimp/defs.ma getl/defs.ma +drop1/props.ma drop/props.ma drop1/defs.ma getl/defs.ma +drop1/defs.ma drop/defs.ma lift1/defs.ma +drop1/getl.ma drop1/defs.ma getl/drop.ma +lift1/props.ma drop1/defs.ma lift/props.ma lift1/defs.ma +lift1/defs.ma lift/defs.ma +lift1/fwd.ma lift/fwd.ma lift1/defs.ma +pr2/pr2.ma getl/props.ma pr0/pr0.ma pr2/defs.ma +pr2/props.ma getl/clear.ma getl/drop.ma pr0/props.ma pr2/defs.ma +pr2/defs.ma getl/defs.ma pr0/defs.ma +pr2/fwd.ma getl/clear.ma getl/drop.ma pr0/fwd.ma pr2/defs.ma +pr2/subst1.ma csubst1/fwd.ma csubst1/getl.ma getl/drop.ma pr0/fwd.ma pr0/subst1.ma pr2/defs.ma subst1/subst1.ma +pr2/clen.ma clen/getl.ma pr2/props.ma +pc3/fsubst0.ma csubst0/getl.ma fsubst0/defs.ma pc3/left.ma +pc3/nf2.ma nf2/pr3.ma pc3/defs.ma +pc3/pc1.ma pc1/defs.ma pc3/defs.ma pr3/pr1.ma +pc3/props.ma pc3/defs.ma pr3/pr3.ma +pc3/left.ma pc3/props.ma +pc3/defs.ma pr3/defs.ma +pc3/fwd.ma pc3/props.ma pr3/fwd.ma +pc3/dec.ma nf2/fwd.ma ty3/arity_props.ma ty3/pr3.ma +pc3/subst1.ma pc3/props.ma pr3/subst1.ma +pc3/wcpr0.ma pc3/props.ma wcpr0/getl.ma +pr0/props.ma pr0/defs.ma subst0/subst0.ma +pr0/pr0.ma lift/tlt.ma pr0/fwd.ma +pr0/defs.ma subst0/defs.ma +pr0/fwd.ma pr0/props.ma +pr0/dec.ma T/dec.ma T/props.ma pr0/fwd.ma subst0/dec.ma +pr0/subst1.ma pr0/props.ma subst1/defs.ma +subst1/props.ma subst0/props.ma subst1/defs.ma +subst1/defs.ma subst0/defs.ma +subst1/fwd.ma subst0/props.ma subst1/defs.ma +subst1/subst1.ma subst0/subst0.ma subst1/fwd.ma +tlt/props.ma tlt/defs.ma +tlt/defs.ma T/defs.ma +r/props.ma r/defs.ma s/defs.ma +r/defs.ma T/defs.ma +wcpr0/defs.ma C/defs.ma pr0/defs.ma +wcpr0/fwd.ma wcpr0/defs.ma +wcpr0/getl.ma getl/props.ma wcpr0/defs.ma +G/defs.ma preamble3.ma +csubst0/drop.ma csubst0/fwd.ma drop/fwd.ma s/props.ma +csubst0/clear.ma clear/fwd.ma csubst0/fwd.ma +csubst0/props.ma csubst0/defs.ma +csubst0/defs.ma C/defs.ma subst0/defs.ma +csubst0/fwd.ma csubst0/defs.ma +csubst0/getl.ma csubst0/clear.ma csubst0/drop.ma getl/fwd.ma +next_plus/props.ma next_plus/defs.ma +next_plus/defs.ma G/defs.ma +tau0/props.ma getl/drop.ma tau0/defs.ma +tau0/defs.ma G/defs.ma getl/defs.ma +csubc/drop.ma csubc/defs.ma sc3/props.ma +csubc/clear.ma csubc/defs.ma +csubc/props.ma csubc/defs.ma sc3/props.ma +csubc/arity.ma arity/defs.ma csubc/csuba.ma +csubc/drop1.ma csubc/drop.ma +csubc/defs.ma sc3/defs.ma +csubc/csuba.ma csuba/defs.ma csubc/defs.ma sc3/props.ma +csubc/getl.ma csubc/clear.ma csubc/drop.ma +arity/props.ma arity/fwd.ma +arity/aprem.ma aprem/props.ma arity/cimp.ma arity/props.ma +arity/pr3.ma arity/subst0.ma csuba/arity.ma pr0/fwd.ma pr1/defs.ma pr3/defs.ma wcpr0/getl.ma +arity/defs.ma getl/defs.ma leq/defs.ma +arity/fwd.ma arity/defs.ma getl/drop.ma leq/asucc.ma leq/fwd.ma +arity/subst0.ma arity/props.ma csubst0/getl.ma csubst0/props.ma fsubst0/fwd.ma getl/getl.ma subst0/dec.ma subst0/fwd.ma +arity/lift1.ma arity/props.ma drop1/defs.ma +arity/cimp.ma arity/defs.ma cimp/props.ma +ex2/props.ma arity/fwd.ma ex2/defs.ma nf2/defs.ma pr2/fwd.ma +ex2/defs.ma C/defs.ma +getl/drop.ma clear/drop.ma getl/props.ma r/props.ma +getl/clear.ma clear/drop.ma getl/props.ma +getl/props.ma clear/props.ma drop/props.ma getl/fwd.ma +getl/defs.ma clear/defs.ma drop/defs.ma +getl/fwd.ma clear/fwd.ma drop/fwd.ma getl/defs.ma +getl/dec.ma getl/props.ma +getl/flt.ma clear/props.ma flt/props.ma getl/fwd.ma +getl/getl.ma getl/clear.ma getl/drop.ma +clear/drop.ma clear/fwd.ma drop/fwd.ma +clear/props.ma clear/fwd.ma +clear/defs.ma C/defs.ma +clear/fwd.ma clear/defs.ma +s/props.ma s/defs.ma +s/defs.ma T/defs.ma +pc1/props.ma pc1/defs.ma pr1/pr1.ma +pc1/defs.ma pr1/defs.ma +sn3/nf2.ma nf2/dec.ma nf2/pr3.ma sn3/defs.ma +sn3/props.ma iso/props.ma nf2/iso.ma pr3/iso.ma sn3/fwd.ma sn3/nf2.ma +sn3/defs.ma pr3/defs.ma +sn3/fwd.ma pr3/props.ma sn3/defs.ma +sn3/lift1.ma drop1/defs.ma lift1/fwd.ma sn3/props.ma +llt/props.ma leq/defs.ma llt/defs.ma +llt/defs.ma A/defs.ma +ex1/props.ma arity/defs.ma ex1/defs.ma leq/props.ma nf2/pr3.ma nf2/props.ma pc3/fwd.ma ty3/fwd.ma +ex1/defs.ma C/defs.ma +ex0/props.ma aplus/props.ma ex0/defs.ma leq/defs.ma +ex0/defs.ma A/defs.ma G/defs.ma +csubst1/props.ma csubst1/defs.ma subst1/defs.ma +csubst1/defs.ma csubst0/defs.ma +csubst1/fwd.ma csubst0/fwd.ma csubst1/defs.ma subst1/props.ma +csubst1/getl.ma csubst0/getl.ma csubst0/props.ma csubst1/props.ma drop/props.ma subst1/props.ma +theory.ma diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/defs.ma index e0b46886f..eea831c6b 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop/defs". + include "C/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/fwd.ma index af9e245f3..bb9c1347c 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop/fwd". + include "drop/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/props.ma index 029720727..e4b21a1a7 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop/props". + include "drop/fwd.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/defs.ma index dea03ca70..2a44cd4d5 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop1/defs". + include "drop/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/getl.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/getl.ma index f8ec287e3..254873dfc 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/getl.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/getl.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop1/getl". + include "drop1/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/props.ma index 5d1e9dc29..1a84d0fe5 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop1/props". + include "drop1/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/defs.ma index 078545c74..a2ce931e4 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex0/defs". + include "A/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/props.ma index 66350ed9c..d293ade39 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex0/props". + include "ex0/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/defs.ma index 3e16c05ed..3963c2b0e 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex1/defs". + include "C/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma index 218efc455..cbba091bc 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex1/props". + include "ex1/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/defs.ma index 482249d5e..5e30cd913 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex2/defs". + include "C/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/props.ma index f35ee3579..85b21716f 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex2/props". + include "ex2/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/defs.ma index 9143b89a2..7ce10924a 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/flt/defs". + include "C/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/props.ma index a8d7daff3..f152ce601 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/flt/props". + include "flt/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/defs.ma index d3eccba43..9d80d9cab 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/fsubst0/defs". + include "csubst0/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/fwd.ma index 773e57278..ae79197b8 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/fsubst0/fwd". + include "fsubst0/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/clear.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/clear.ma index 8b7c55259..f7b873198 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/clear.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/clear.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/clear". + include "getl/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/dec.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/dec.ma index f22b7b333..17082d903 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/dec.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/dec.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/dec". + include "getl/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/defs.ma index 0d97227a1..c7e9a4ffb 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/defs". + include "drop/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/drop.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/drop.ma index c176ca62d..67607225f 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/drop.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/drop.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/drop". + include "getl/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/flt.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/flt.ma index 81a47ff2e..aa9461616 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/flt.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/flt.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/flt". + include "getl/fwd.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/fwd.ma index 538165227..99bf27b3f 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/fwd". + include "getl/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/getl.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/getl.ma index 62218d746..6ab30e2b8 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/getl.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/getl.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/getl". + include "getl/drop.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/props.ma index a5228d950..0f49cdaac 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/props". + include "getl/fwd.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/defs.ma index fa327f922..46e832ff6 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/iso/defs". + include "T/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/fwd.ma index 5a6607941..fc801e762 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/iso/fwd". + include "iso/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/props.ma index edc9758a9..0393ee140 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/iso/props". + include "iso/fwd.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/asucc.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/asucc.ma index 25f9dfd07..73fff7f79 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/asucc.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/asucc.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/leq/asucc". + include "leq/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/defs.ma index d14a0e535..83f68a21a 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/leq/defs". + include "aplus/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/fwd.ma index 36c26579b..649eb872b 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/leq/fwd". + include "leq/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/props.ma index 0ad16f9e7..d879be152 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/leq/props". + include "leq/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/defs.ma index 9a03fcd17..de61fc39f 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift/defs". + include "T/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma index 5a80f43e6..a68695a33 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift/fwd". + include "lift/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma index 6a8cc0ac0..3805df7db 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift/props". + include "tlist/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma index 0e041d02d..316ebe839 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift/tlt". + include "lift/fwd.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/defs.ma index 4042efeee..3764b6b25 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift1/defs". + include "lift/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/fwd.ma index bbdef6d1f..426af9e10 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift1/fwd". + include "lift1/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma index db5d76536..7b8ce0c79 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift1/props". + include "lift1/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/defs.ma index 19ef14486..ba4d1f3ba 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/llt/defs". + include "A/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/props.ma index d34488300..22fcde732 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/llt/props". + include "llt/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/makefile b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/makefile deleted file mode 100644 index 8f20b3276..000000000 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/makefile +++ /dev/null @@ -1,39 +0,0 @@ -H=@ - -RT_BASEDIR=../../../ -OPTIONS=-bench -onepass -system -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) $(@:.opt=) - -preall: - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel) - -preall.opt: - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) init $(devel) diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/defs.ma index 1764e8610..f5922b8e7 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/next_plus/defs". + include "G/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/props.ma index e0f2654ac..57f461e50 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/next_plus/props". + include "next_plus/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/arity.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/arity.ma index d67f67282..75db60a37 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/arity.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/arity.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/arity". + include "nf2/fwd.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/dec.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/dec.ma index d7aa80992..25245ac11 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/dec.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/dec.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/dec". + include "nf2/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/defs.ma index 23868ee8b..b219352e9 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/defs". + include "pr2/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/fwd.ma index 849e86090..531f5979b 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/fwd". + include "nf2/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/iso.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/iso.ma index 54b097c04..7d90db0fc 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/iso.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/iso.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/iso". + include "nf2/pr3.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/lift1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/lift1.ma index 33c44778d..9049b7518 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/lift1.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/lift1.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/lift1". + include "nf2/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/pr3.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/pr3.ma index 2206469dc..b33e7c851 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/pr3.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/pr3.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/pr3". + include "nf2/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma index 499cd5fdc..47c82fd63 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/props". + include "nf2/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/defs.ma index c81142f5d..20029263c 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc1/defs". + include "pr1/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/props.ma index 0bd48d44c..279297229 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc1/props". + include "pc1/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/dec.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/dec.ma index 01f4fc13b..9877b5b84 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/dec.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/dec.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/dec". + include "ty3/arity_props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/defs.ma index 91d5eaf8b..c475349cf 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/defs". + include "pr3/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fsubst0.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fsubst0.ma index 6ab7daf1c..e286c315d 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fsubst0.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fsubst0.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/fsubst0". + include "pc3/left.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fwd.ma index cd70ecf45..9c94e0f44 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/fwd". + include "pc3/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/left.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/left.ma index 3a6db7706..a44249eea 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/left.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/left.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/left". + include "pc3/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/nf2.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/nf2.ma index 41136207b..7bd86cafc 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/nf2.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/nf2.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/nf2". + include "pc3/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/pc1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/pc1.ma index 0893239e4..7d592cbbc 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/pc1.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/pc1.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/pc1". + include "pc3/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/props.ma index 98a40de4e..f72ad7a2b 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/props". + include "pc3/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/subst1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/subst1.ma index 510b2d649..6a9dd2464 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/subst1.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/subst1.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/subst1". + include "pc3/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/wcpr0.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/wcpr0.ma index 5ed59a431..e1a302b8e 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/wcpr0.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/wcpr0.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/wcpr0". + include "pc3/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/dec.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/dec.ma index 26c4a21b6..429de32f7 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/dec.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/dec.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/dec". + include "pr0/fwd.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/defs.ma index 4086f5beb..8f4ecf549 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/defs". + include "subst0/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/fwd.ma index 5d1ef3b24..1adb47749 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/fwd". + include "pr0/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0.ma index 59e04cef8..00f623b69 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0". + include "pr0/fwd.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/props.ma index 5e8396c47..18496c895 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/props". + include "pr0/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/subst1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/subst1.ma index 0aa55239f..f5722a372 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/subst1.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/subst1.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/subst1". + include "pr0/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/defs.ma index 85540bde7..7a551d6b4 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr1/defs". + include "pr0/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/pr1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/pr1.ma index 98a21a512..3aae64c40 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/pr1.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/pr1.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr1/pr1". + include "pr1/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/props.ma index 7840b3cd2..330d11f05 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr1/props". + include "pr1/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/clen.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/clen.ma index 27275fa3a..e354ba5c4 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/clen.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/clen.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/clen". + include "pr2/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/defs.ma index 77932c984..743e68703 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/defs". + include "pr0/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd.ma index 848d216fa..7333bbf05 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd". + include "pr2/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/pr2.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/pr2.ma index 307d55398..d060f68a0 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/pr2.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/pr2.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/pr2". + include "pr2/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/props.ma index 2cb35e582..2f8498c59 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/props". + include "pr2/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1.ma index 27a0221d5..051b6d50e 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1". + include "pr2/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/defs.ma index 3baff8a16..a53549dde 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/defs". + include "pr2/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/fwd.ma index 5e6137217..32626a34c 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/fwd". + include "pr3/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/iso.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/iso.ma index 1f628e9b2..7ec0ba521 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/iso.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/iso.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/iso". + include "pr3/fwd.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr1.ma index 21344033e..df0a92d5b 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr1.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr1.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/pr1". + include "pr3/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr3.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr3.ma index c29781a0e..c3511368c 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr3.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr3.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/pr3". + include "pr3/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/props.ma index c07efa64d..fa44c4bf3 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/props". + include "pr3/pr1.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/subst1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/subst1.ma index 4894993fc..b6e5688be 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/subst1.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/subst1.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/subst1". + include "pr3/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/wcpr0.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/wcpr0.ma index dd20dae41..0d8c422ba 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/wcpr0.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/wcpr0.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/wcpr0". + include "pr3/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble3.ma similarity index 96% rename from matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble3.ma index f9dc333af..4bff57162 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble3.ma @@ -12,9 +12,9 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/preamble". -include "../Base-1/theory.ma". + +include "theory.ma". alias id "and_ind" = "cic:/Coq/Init/Logic/and_ind.con". alias id "bool_ind" = "cic:/Coq/Init/Datatypes/bool_ind.con". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/defs.ma index 005f3a107..08a744024 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/r/defs". + include "T/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/props.ma index 505d1e450..f494453e7 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/r/props". + include "r/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/root b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/root new file mode 100644 index 000000000..cca019073 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/root @@ -0,0 +1,2 @@ +baseuri=cic:/matita/LAMBDA-TYPES/LambdaDelta-1 +include_paths= ../Base-1 diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/defs.ma index 6cb9d340f..8c499e16d 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/s/defs". + include "T/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/props.ma index 7acdf612f..f77a611e5 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/s/props". + include "s/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/arity.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/arity.ma index e7f13ac61..0f1ed1937 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/arity.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/arity.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sc3/arity". + include "csubc/arity.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/defs.ma index fd161f395..ae5754fb9 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sc3/defs". + include "sn3/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/props.ma index c1d3787b8..2bdf487cf 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sc3/props". + include "sc3/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/defs.ma index 0d38de3a8..92be59104 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sn3/defs". + include "pr3/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/fwd.ma index 779e4a8cf..1283e6967 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sn3/fwd". + include "sn3/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/lift1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/lift1.ma index d84d094a2..3428c0e63 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/lift1.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/lift1.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sn3/lift1". + include "sn3/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/nf2.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/nf2.ma index 7b5c1d1bb..fa21c378f 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/nf2.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/nf2.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sn3/nf2". + include "sn3/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma index 8cdfff89e..b47e2a185 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sn3/props". + include "sn3/nf2.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare3.ma similarity index 99% rename from matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare3.ma index 70b94347b..891665097 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare3.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/spare". + include "theory.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/dec.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/dec.ma index cfa2bbe3f..2f299659b 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/dec.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/dec.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/dec". + include "subst0/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/defs.ma index c675bc6ab..c2e4e2161 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/defs". + include "lift/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd.ma index e16f362b0..c710b9670 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd". + include "subst0/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma index 7b147c20e..fc02e10ce 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/props". + include "subst0/fwd.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/subst0.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/subst0.ma index 9b9c0bb54..89253ee4e 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/subst0.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/subst0.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/subst0". + include "subst0/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt.ma index fd0ba2f0c..4d2195d14 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt". + include "subst0/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/defs.ma index 304adc590..56a33fe6c 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst1/defs". + include "subst0/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/fwd.ma index 317086097..2db6e6c65 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst1/fwd". + include "subst1/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/props.ma index a933775b7..ef21270ff 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst1/props". + include "subst1/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/subst1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/subst1.ma index dc20f3ff3..514dd8f99 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/subst1.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/subst1.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst1/subst1". + include "subst1/fwd.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/defs.ma index 0a1853ded..8fac9e2d5 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tau0/defs". + include "G/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/props.ma index 9baf6cb96..c3e134c10 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tau0/props". + include "tau0/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/cnt.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/cnt.ma index 845ea8933..3a5824df6 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/cnt.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/cnt.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tau1/cnt". + include "tau1/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/defs.ma index 09a531fbc..ced0a2668 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tau1/defs". + include "tau0/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/props.ma index 30ee3158c..d74e3bfa6 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tau1/props". + include "tau1/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory3.ma similarity index 95% rename from matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma rename to matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory3.ma index daf2a250e..b0d977422 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory3.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/theory". + include "subst0/tlt.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/defs.ma index ad412abf3..144bb25e1 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tlist/defs". + include "T/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/props.ma index 9f37ad2b4..6ee6bf5d8 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tlist/props". + include "tlist/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/defs.ma index f5acb3e27..63c0ce597 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tlt/defs". + include "T/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/props.ma index b75bc8053..2e3cfc998 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tlt/props". + include "tlt/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity.ma index ba58219da..5dba1793e 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/arity". + include "ty3/pr3_props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props.ma index 2f758d80c..0e221591c 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props". + include "ty3/arity.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/dec.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/dec.ma index 4ad1efbd4..9357365d7 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/dec.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/dec.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/dec". + include "ty3/pr3_props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/defs.ma index eff4d8e7b..a91d36ccd 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs". + include "G/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma index 1370b3d79..9fa96ff7f 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0". + include "ty3/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fwd.ma index 5267f5c6a..bc861903c 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/fwd". + include "ty3/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma index 358626faa..300238885 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2". + include "ty3/arity.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma index d0f9999d4..dc9fde8e6 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3". + include "csubt/ty3.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma index 4693788ce..fd73008bb 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props". + include "ty3/pr3.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma index 9809bc5ef..7fbddf8eb 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/props". + include "ty3/fwd.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma index 60e08dbe1..44d68dd1b 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1". + include "ty3/props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma index a470e0d0c..2055522bf 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0". + include "ty3/pr3_props.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/defs.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/defs.ma index dff8bb8cc..28aca266a 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/defs.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/wcpr0/defs". + include "pr0/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/fwd.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/fwd.ma index 359d38544..adde06ff8 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/fwd.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/fwd.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/wcpr0/fwd". + include "wcpr0/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/getl.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/getl.ma index f52805131..1f5e14c44 100644 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/getl.ma +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/getl.ma @@ -14,7 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/wcpr0/getl". + include "wcpr0/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma index b8a4e2a85..fb71d3976 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/defs.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/defs". + (* LIFT RELATION - Usage: invoke with positive polarity diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fun.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fun.ma index 86e8031b4..d26bdb0e7 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fun.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/fun.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/fun". + include "Lift/inv.ma". diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma index 95630e43e..bbd8d744e 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/inv.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/inv". + include "Lift/defs.ma". diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma index 9df9cbd63..8e50c477b 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Lift/props.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/Lift/props". + include "Lift/fun.ma". diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/Makefile b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Makefile new file mode 100644 index 000000000..29cae5c9b --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/Makefile @@ -0,0 +1,10 @@ +DIR=$(shell basename $$PWD) + +$(DIR) all: + ../../../matitac +$(DIR).opt opt all.opt: + ../../../matitac.opt +clean: + ../../../matitaclean +clean.opt: + ../../../matitaclean.opt diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Context.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Context.ma index f5c63fd0b..d63ffcf2e 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Context.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Context.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/datatypes/Context". + (* FLAT CONTEXTS - Naming policy: diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma index a7f5e7f07..e1f090d1a 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/datatypes/Term.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/datatypes/Term". + (* POLARIZED TERMS - Naming policy: @@ -24,7 +24,7 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/datatypes/Term". - terms : t u *) -include "preamble.ma". +include "preamble4.ma". inductive Bind: Type \def | abbr: Bind diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/depends b/matita/contribs/LAMBDA-TYPES/Unified-Sub/depends new file mode 100644 index 000000000..82206df5e --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/depends @@ -0,0 +1,12 @@ +preamble4.ma NLE/nplus.ma NLE/props.ma NPlus/monoid.ma datatypes/Bool.ma logic/equality.ma +datatypes/Context.ma datatypes/Term.ma +datatypes/Term.ma preamble4.ma +Lift/props.ma Lift/fun.ma +Lift/inv.ma Lift/defs.ma +Lift/defs.ma datatypes/Term.ma +Lift/fun.ma Lift/inv.ma +NLE/nplus.ma +NLE/props.ma +NPlus/monoid.ma +datatypes/Bool.ma +logic/equality.ma diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/makefile b/matita/contribs/LAMBDA-TYPES/Unified-Sub/makefile deleted file mode 100644 index d7a63e5f1..000000000 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/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) $(@:.opt=) - -preall: - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel) - -preall.opt: - $(H)$(XXX) MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) init $(devel) diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble4.ma similarity index 85% rename from matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma rename to matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble4.ma index d889c3995..1449c154f 100644 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble4.ma @@ -14,16 +14,16 @@ (* Project started Tue Aug 22, 2006 ***************************************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Unified-Sub/preamble". + (* PREAMBLE *) include "logic/equality.ma". -include "../../RELATIONAL/datatypes/Bool.ma". -include "../../RELATIONAL/NPlus/monoid.ma". -include "../../RELATIONAL/NLE/props.ma". -include "../../RELATIONAL/NLE/nplus.ma". +include "datatypes/Bool.ma". +include "NPlus/monoid.ma". +include "NLE/props.ma". +include "NLE/nplus.ma". axiom f_equal_3: \forall (A,B,C,D:Set). \forall (f:A \to B \to C \to D). diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/root b/matita/contribs/LAMBDA-TYPES/Unified-Sub/root new file mode 100644 index 000000000..e3402e0be --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/root @@ -0,0 +1,2 @@ +baseuri=cic:/matita/LAMBDA-TYPES/Unified-Sub +include_paths= ../../RELATIONAL/ diff --git a/matita/contribs/prova.ma b/matita/contribs/prova.ma deleted file mode 100644 index a0cab9867..000000000 --- a/matita/contribs/prova.ma +++ /dev/null @@ -1,236 +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/test/prova". - -include "../legacy/coq.ma". - -theorem pippo: \forall (A,B:Prop). A \land B \to A. - intros; decompose; assumption. -qed. - -inline procedural "cic:/matita/test/prova/pippo.con". - -alias id "plus" = "cic:/Coq/Init/Peano/plus.con". -alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". -alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)". -theorem plus_comm: \forall n:nat.\forall m:nat.eq nat (plus n m) (plus m n). - intros; alias id "plus_comm" = "cic:/Coq/Arith/Plus/plus_comm.con". -apply plus_comm. -qed. -(* -include "LAMBDA-TYPES/LambdaDelta-1/preamble.ma". -alias id "ty3" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs/ty3.ind#xpointer(1/1)". -alias id "pc3" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/defs/pc3.con". -alias id "THead" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/T.ind#xpointer(1/1/3)". -alias id "T" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/T.ind#xpointer(1/1)". -alias id "G" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/G/defs/G.ind#xpointer(1/1)". -alias id "Flat" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/K.ind#xpointer(1/1/2)". -alias id "Cast" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/F.ind#xpointer(1/1/2)". -alias id "C" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/C/defs/C.ind#xpointer(1/1)". -theorem ty3_gen_cast: - (\forall g:G - .\forall c:C - .\forall t1:T - .\forall t2:T - .\forall x:T - .ty3 g c (THead (Flat Cast) t2 t1) x - \rarr pc3 c t2 x\land ty3 g c t1 t2) -. -(* tactics: 80 *) -intros 6 (g c t1 t2 x H). -apply insert_eq;(* 6 P P P C I I 3 0 *) -[apply T(* dependent *) -|apply (THead (Flat Cast) t2 t1)(* dependent *) -|apply (\lambda t:T.ty3 g c t x)(* dependent *) -|intros 2 (y H0). -alias id "ty3_ind" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs/ty3_ind.con". -elim H0 using ty3_ind names 0;(* 13 P C I I I I I I I C C C I 12 3 *) -[intros 11 (c0 t0 t UNUSED UNUSED u t3 UNUSED H4 H5 H6). -letin H7 \def (f_equal T T (\lambda e:T.e) u (THead (Flat Cast) t2 t1) H6).(* 6 C C C C C I *) -rewrite > H7 in H4:(%) as (H8). -cut (pc3 c0 t2 t3\land ty3 g c0 t1 t2) as H10; -[id -|apply H8.(* 1 I *) -apply refl_equal(* 2 C C *) -]. -elim H10 using and_ind names 0.(* 5 P P C I I 3 0 *) -intros 2 (H11 H12). -apply conj;(* 4 C C I I *) -[alias id "pc3_t" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/props/pc3_t.con". -apply pc3_t;(* 6 P C C I C I *) -[apply t3(* dependent *) -|apply H11(* assumption *) -|apply H5(* assumption *) -] -|apply H12(* assumption *) -] -|intros 3 (c0 m H1). -alias id "K" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/K.ind#xpointer(1/1)". -cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with -[TSort (_:nat)\rArr True -|TLRef (_:nat)\rArr False -|THead (_:K) (_:T) (_:T)\rArr False] as H2; -[id -|rewrite < H1 in \vdash (%). -apply I -]. -clearbody H2. -change in H2:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with -[TSort (_:nat)\rArr True -|TLRef (_:nat)\rArr False -|THead (_:K) (_:T) (_:T)\rArr False]. -elim H2 using False_ind names 0(* 2 C I 2 0 *) -|intros 9 (n c0 d u UNUSED t UNUSED UNUSED H4). -cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with -[TSort (_:nat)\rArr False -|TLRef (_:nat)\rArr True -|THead (_:K) (_:T) (_:T)\rArr False] as H5; -[id -|rewrite < H4 in \vdash (%). -apply I -]. -clearbody H5. -change in H5:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with -[TSort (_:nat)\rArr False -|TLRef (_:nat)\rArr True -|THead (_:K) (_:T) (_:T)\rArr False]. -elim H5 using False_ind names 0(* 2 C I 2 0 *) -|intros 9 (n c0 d u UNUSED t UNUSED UNUSED H4). -cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with -[TSort (_:nat)\rArr False -|TLRef (_:nat)\rArr True -|THead (_:K) (_:T) (_:T)\rArr False] as H5; -[id -|rewrite < H4 in \vdash (%). -apply I -]. -clearbody H5. -change in H5:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with -[TSort (_:nat)\rArr False -|TLRef (_:nat)\rArr True -|THead (_:K) (_:T) (_:T)\rArr False]. -elim H5 using False_ind names 0(* 2 C I 2 0 *) -|intros 14 (c0 u t UNUSED UNUSED b t0 t3 UNUSED UNUSED t4 UNUSED UNUSED H7). -alias id "F" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/F.ind#xpointer(1/1)". -alias id "B" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/B.ind#xpointer(1/1)". -cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with -[TSort (_:nat)\rArr False -|TLRef (_:nat)\rArr False -|THead (k:K) (_:T) (_:T)\rArr - match k in K return \lambda _:K.Prop with - [Bind (_:B)\rArr True|Flat (_:F)\rArr False]] as H8; -[id -|rewrite < H7 in \vdash (%). -apply I -]. -clearbody H8. -change in H8:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with -[TSort (_:nat)\rArr False -|TLRef (_:nat)\rArr False -|THead (k:K) (_:T) (_:T)\rArr - match k in K return \lambda _:K.Prop with - [Bind (_:B)\rArr True|Flat (_:F)\rArr False]]. -elim H8 using False_ind names 0(* 2 C I 2 0 *) -|intros 10 (c0 w u UNUSED UNUSED v t UNUSED UNUSED H5). -cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with -[TSort (_:nat)\rArr False -|TLRef (_:nat)\rArr False -|THead (k:K) (_:T) (_:T)\rArr - match k in K return \lambda _:K.Prop with - [Bind (_:B)\rArr False - |Flat (f:F)\rArr - match f in F return \lambda _:F.Prop with - [Appl\rArr True|Cast\rArr False]]] as H6; -[id -|rewrite < H5 in \vdash (%). -apply I -]. -clearbody H6. -change in H6:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with -[TSort (_:nat)\rArr False -|TLRef (_:nat)\rArr False -|THead (k:K) (_:T) (_:T)\rArr - match k in K return \lambda _:K.Prop with - [Bind (_:B)\rArr False - |Flat (f:F)\rArr - match f in F return \lambda _:F.Prop with - [Appl\rArr True|Cast\rArr False]]]. -elim H6 using False_ind names 0(* 2 C I 2 0 *) -|intros 9 (c0 t0 t3 H1 H2 t4 UNUSED UNUSED H5). -letin H6 \def (f_equal T T - (\lambda e:T - .match e in T return \lambda _:T.T with - [TSort (_:nat)\rArr t3 - |TLRef (_:nat)\rArr t3 - |THead (_:K) (t:T) (_:T)\rArr t]) (THead (Flat Cast) t3 t0) - (THead (Flat Cast) t2 t1) H5).(* 6 C C C C C I *) -letin H7 \def (f_equal T T - (\lambda e:T - .match e in T return \lambda _:T.T with - [TSort (_:nat)\rArr t0 - |TLRef (_:nat)\rArr t0 - |THead (_:K) (_:T) (t:T)\rArr t]) (THead (Flat Cast) t3 t0) - (THead (Flat Cast) t2 t1) H5).(* 6 C C C C C I *) -cut (t3=t2\rarr pc3 c0 t2 t3\land ty3 g c0 t1 t2) as DEFINED; -[id -|intros 1 (H8). -rewrite > H8 in H2:(%) as (UNUSED). -rewrite > H8 in H1:(%) as (H12). -rewrite > H8 in \vdash (%). -clearbody H7. -change in H7:(%) with (match THead (Flat Cast) t3 t0 in T return \lambda _:T.T with - [TSort (_:nat)\rArr t0 - |TLRef (_:nat)\rArr t0 - |THead (_:K) (_:T) (t:T)\rArr t] - =match THead (Flat Cast) t2 t1 in T return \lambda _:T.T with - [TSort (_:nat)\rArr t0 - |TLRef (_:nat)\rArr t0 - |THead (_:K) (_:T) (t:T)\rArr t]). -rewrite > H7 in H12:(%) as (H14). -apply conj;(* 4 C C I I *) -[alias id "pc3_refl" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/props/pc3_refl.con". -apply pc3_refl(* 2 C C *) -|apply H14(* assumption *) -] -]. -apply DEFINED.(* 1 I *) -apply H6(* assumption *) -] -|apply H(* assumption *) -]. -qed. -*) -(* -include "nat/orders.ma". - -theorem le_inv: - \forall P:nat \to Prop - .\forall p2 - .\forall p1 - .p2 <= p1 \to - (p1 = p2 \to P p2) \to - (\forall n1 - .p2 <= n1 \to - (p1 = n1 \to P n1) \to - p1 = S n1 \to P (S n1)) \to - P p1. - intros 4; elim H names 0; clear H p1; intros; - [ apply H; reflexivity - | apply H3; clear H3; intros; - [ apply H | apply H1; clear H1; intros; subst; - [ apply H2; apply H3 | ] - | reflexivity - ] -*) -- 2.39.2