From: Enrico Tassi Date: Thu, 10 Jan 2008 10:45:04 +0000 (+0000) Subject: contribs should now compile X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=711e170c2deaa92289d9d4eb7c0e8aedbe62b5cb;p=helm.git contribs should now compile --- 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/defs.mma deleted file mode 100644 index 12438b398..000000000 --- a/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs.mma +++ /dev/null @@ -1,23 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/blt/defs". - -include "preamble.ma". - - -(* object blt not inlined *) - diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs2.mma b/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs2.mma new file mode 100644 index 000000000..6eb948342 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/blt/defs2.mma @@ -0,0 +1,20 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +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/props.mma deleted file mode 100644 index d24466394..000000000 --- a/matita/contribs/LAMBDA-TYPES/Base-2/blt/props.mma +++ /dev/null @@ -1,28 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/blt/props". - -include "blt/defs.ma". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/lt_blt.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/le_bge.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/blt_lt.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/bge_le.con". - diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/blt/props2.mma b/matita/contribs/LAMBDA-TYPES/Base-2/blt/props2.mma new file mode 100644 index 000000000..1fd2047fd --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/blt/props2.mma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +include "blt/defs2.ma". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/lt_blt.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/le_bge.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/blt_lt.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/blt/props/bge_le.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/arith.mma deleted file mode 100644 index ee4663a51..000000000 --- a/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith.mma +++ /dev/null @@ -1,112 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/ext/arith". - -include "preamble.ma". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/nat_dec.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/simpl_plus_r.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_plus_r.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_permute_2_in_3.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_permute_2_in_3_assoc.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_O.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_Sx_SO.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/eq_nat_dec.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/neq_eq_e.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_false.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_Sx_x.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_n_pred.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_le.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_plus_minus_sym.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus_minus.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus_plus.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_trans_plus_r.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_O.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_gen_S.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_plus_x_Sy.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/simpl_lt_plus_r.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_x_Sy.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_plus_minus.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_plus_minus_r.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_x_SO.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_x_pred_y.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_le_minus.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_le_e.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_eq_e.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_eq_gt_e.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_gen_xS.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_lt_false.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_neq.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/arith0.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/O_minus.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_minus.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_plus.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_S_minus.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_pred_y.con". - diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith2.mma b/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith2.mma new file mode 100644 index 000000000..436b497c9 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/ext/arith2.mma @@ -0,0 +1,110 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +include "preamble.ma". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/nat_dec.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/simpl_plus_r.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_plus_r.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_permute_2_in_3.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_permute_2_in_3_assoc.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_O.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_Sx_SO.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/eq_nat_dec.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/neq_eq_e.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_false.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_Sx_x.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_n_pred.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_le.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_plus_minus_sym.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus_minus.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus_plus.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_minus.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_trans_plus_r.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_O.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_gen_S.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_plus_x_Sy.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/simpl_lt_plus_r.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_x_Sy.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_plus_minus.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_plus_minus_r.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_x_SO.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_x_pred_y.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_le_minus.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_le_e.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_eq_e.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_eq_gt_e.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_gen_xS.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_lt_false.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_neq.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/arith0.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/O_minus.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/minus_minus.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/plus_plus.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/le_S_minus.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith/lt_x_pred_y.con". + diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma b/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma deleted file mode 100644 index 18de7f71a..000000000 --- a/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics.mma +++ /dev/null @@ -1,27 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/ext/tactics". - -include "preamble.ma". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/insert_eq.con". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/unintro.con". - -inline procedural -"cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/xinduction.con". - diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics2.mma b/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics2.mma new file mode 100644 index 000000000..e6b75198a --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/ext/tactics2.mma @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +include "preamble.ma". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/insert_eq.con". + +inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/unintro.con". + +inline procedural +"cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics/xinduction.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/defs.mma deleted file mode 100644 index 3dc03da0b..000000000 --- a/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs.mma +++ /dev/null @@ -1,32 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/plist/defs". - -include "preamble.ma". - - -(* object PList not inlined *) - - -(* object PConsTail not inlined *) - - -(* object Ss not inlined *) - - -(* object papp not inlined *) - diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs2.mma b/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs2.mma new file mode 100644 index 000000000..4ae6d5156 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/plist/defs2.mma @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +include "preamble.ma". + + +(* object PList not inlined *) + + +(* object PConsTail not inlined *) + + +(* object Ss not inlined *) + + +(* object papp not inlined *) + diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma b/matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma deleted file mode 100644 index 29357a88a..000000000 --- a/matita/contribs/LAMBDA-TYPES/Base-2/plist/props.mma +++ /dev/null @@ -1,22 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/plist/props". - -include "plist/defs.ma". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/plist/props/papp_ss.con". - diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/plist/props2.mma b/matita/contribs/LAMBDA-TYPES/Base-2/plist/props2.mma new file mode 100644 index 000000000..f9cec902e --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/plist/props2.mma @@ -0,0 +1,20 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +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/theory.mma deleted file mode 100644 index 1adab3e2b..000000000 --- a/matita/contribs/LAMBDA-TYPES/Base-2/theory.mma +++ /dev/null @@ -1,28 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/theory". - -include "ext/tactics.ma". - -include "ext/arith.ma". - -include "types/props.ma". - -include "blt/props.ma". - -include "plist/props.ma". - diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/theory2.mma b/matita/contribs/LAMBDA-TYPES/Base-2/theory2.mma new file mode 100644 index 000000000..d1a0ca8b4 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/theory2.mma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +include "ext/tactics2.ma". + +include "ext/arith2.ma". + +include "types/props2.ma". + +include "blt/props2.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/defs.mma deleted file mode 100644 index 000f283aa..000000000 --- a/matita/contribs/LAMBDA-TYPES/Base-2/types/defs.mma +++ /dev/null @@ -1,80 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/types/defs". - -include "preamble.ma". - - -(* object and3 not inlined *) - - -(* object and4 not inlined *) - - -(* object or3 not inlined *) - - -(* object or4 not inlined *) - - -(* object ex3 not inlined *) - - -(* object ex4 not inlined *) - - -(* object ex_2 not inlined *) - - -(* object ex2_2 not inlined *) - - -(* object ex3_2 not inlined *) - - -(* object ex4_2 not inlined *) - - -(* object ex_3 not inlined *) - - -(* object ex2_3 not inlined *) - - -(* object ex3_3 not inlined *) - - -(* object ex4_3 not inlined *) - - -(* object ex3_4 not inlined *) - - -(* object ex4_4 not inlined *) - - -(* object ex4_5 not inlined *) - - -(* object ex5_5 not inlined *) - - -(* object ex6_6 not inlined *) - - -(* object ex6_7 not inlined *) - diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/types/defs2.mma b/matita/contribs/LAMBDA-TYPES/Base-2/types/defs2.mma new file mode 100644 index 000000000..594edd269 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/types/defs2.mma @@ -0,0 +1,78 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +include "preamble.ma". + + +(* object and3 not inlined *) + + +(* object and4 not inlined *) + + +(* object or3 not inlined *) + + +(* object or4 not inlined *) + + +(* object ex3 not inlined *) + + +(* object ex4 not inlined *) + + +(* object ex_2 not inlined *) + + +(* object ex2_2 not inlined *) + + +(* object ex3_2 not inlined *) + + +(* object ex4_2 not inlined *) + + +(* object ex_3 not inlined *) + + +(* object ex2_3 not inlined *) + + +(* object ex3_3 not inlined *) + + +(* object ex4_3 not inlined *) + + +(* object ex3_4 not inlined *) + + +(* object ex4_4 not inlined *) + + +(* object ex4_5 not inlined *) + + +(* object ex5_5 not inlined *) + + +(* object ex6_6 not inlined *) + + +(* object ex6_7 not inlined *) + diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma b/matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma deleted file mode 100644 index d79bfc46b..000000000 --- a/matita/contribs/LAMBDA-TYPES/Base-2/types/props.mma +++ /dev/null @@ -1,22 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/types/props". - -include "types/defs.ma". - -inline procedural "cic:/matita/LAMBDA-TYPES/Base-1/types/props/ex2_sym.con". - diff --git a/matita/contribs/LAMBDA-TYPES/Base-2/types/props2.mma b/matita/contribs/LAMBDA-TYPES/Base-2/types/props2.mma new file mode 100644 index 000000000..10b502461 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Base-2/types/props2.mma @@ -0,0 +1,20 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + +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/definitions.ma deleted file mode 100644 index 620154782..000000000 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions.ma +++ /dev/null @@ -1,62 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/definitions". - -include "tlt/defs.ma". - -include "iso/defs.ma". - -include "clen/defs.ma". - -include "flt/defs.ma". - -include "cnt/defs.ma". - -include "cimp/defs.ma". - -include "subst1/defs.ma". - -include "csubst1/defs.ma". - -include "fsubst0/defs.ma". - -include "next_plus/defs.ma". - -include "tau1/defs.ma". - -include "llt/defs.ma". - -include "aprem/defs.ma". - -include "ex0/defs.ma". - -include "wcpr0/defs.ma". - -include "csuba/defs.ma". - -include "nf2/defs.ma". - -include "ex2/defs.ma". - -include "csubc/defs.ma". - -include "pc1/defs.ma". - -include "ex1/defs.ma". - -include "csubt/defs.ma". - diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions3.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions3.ma new file mode 100644 index 000000000..61d77ed54 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions3.ma @@ -0,0 +1,62 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + + + +include "tlt/defs.ma". + +include "iso/defs.ma". + +include "clen/defs.ma". + +include "flt/defs.ma". + +include "cnt/defs.ma". + +include "cimp/defs.ma". + +include "subst1/defs.ma". + +include "csubst1/defs.ma". + +include "fsubst0/defs.ma". + +include "next_plus/defs.ma". + +include "tau1/defs.ma". + +include "llt/defs.ma". + +include "aprem/defs.ma". + +include "ex0/defs.ma". + +include "wcpr0/defs.ma". + +include "csuba/defs.ma". + +include "nf2/defs.ma". + +include "ex2/defs.ma". + +include "csubc/defs.ma". + +include "pc1/defs.ma". + +include "ex1/defs.ma". + +include "csubt/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/preamble.ma deleted file mode 100644 index f9dc333af..000000000 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble.ma +++ /dev/null @@ -1,42 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/preamble". - -include "../Base-1/theory.ma". - -alias id "and_ind" = "cic:/Coq/Init/Logic/and_ind.con". -alias id "bool_ind" = "cic:/Coq/Init/Datatypes/bool_ind.con". -alias id "ex" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)". -alias id "ex_ind" = "cic:/Coq/Init/Logic/ex_ind.con". -alias id "ex_intro" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1/1)". -alias id "f_equal2" = "cic:/Coq/Init/Logic/f_equal2.con". -alias id "f_equal3" = "cic:/Coq/Init/Logic/f_equal3.con". -alias id "le_antisym" = "cic:/Coq/Arith/Le/le_antisym.con". -alias id "le_lt_trans" = "cic:/Coq/Arith/Lt/le_lt_trans.con". -alias id "le_plus_trans" = "cic:/Coq/Arith/Plus/le_plus_trans.con". -alias id "lt_le_trans" = "cic:/Coq/Arith/Lt/lt_le_trans.con". -alias id "lt_n_Sn" = "cic:/Coq/Arith/Lt/lt_n_Sn.con". -alias id "lt_S_n" = "cic:/Coq/Arith/Lt/lt_S_n.con". -alias id "lt_trans" = "cic:/Coq/Arith/Lt/lt_trans.con". -alias id "lt_wf_ind" = "cic:/Coq/Arith/Wf_nat/lt_wf_ind.con". -alias id "minus_n_n" = "cic:/Coq/Arith/Minus/minus_n_n.con". -alias id "minus_Sn_m" = "cic:/Coq/Arith/Minus/minus_Sn_m.con". -alias id "plus_le_lt_compat" = "cic:/Coq/Arith/Plus/plus_le_lt_compat.con". -alias id "plus_lt_compat" = "cic:/Coq/Arith/Plus/plus_lt_compat.con". -alias id "plus_lt_compat_r" = "cic:/Coq/Arith/Plus/plus_lt_compat_r.con". -alias id "plus_lt_le_compat" = "cic:/Coq/Arith/Plus/plus_lt_le_compat.con". -alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con". -alias id "plus_Snm_nSm" = "cic:/Coq/Arith/Plus/plus_Snm_nSm.con". -alias id "S_pred" = "cic:/Coq/Arith/Lt/S_pred.con". diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble3.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble3.ma new file mode 100644 index 000000000..4bff57162 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/preamble3.ma @@ -0,0 +1,42 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + + + +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". +alias id "ex" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)". +alias id "ex_ind" = "cic:/Coq/Init/Logic/ex_ind.con". +alias id "ex_intro" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1/1)". +alias id "f_equal2" = "cic:/Coq/Init/Logic/f_equal2.con". +alias id "f_equal3" = "cic:/Coq/Init/Logic/f_equal3.con". +alias id "le_antisym" = "cic:/Coq/Arith/Le/le_antisym.con". +alias id "le_lt_trans" = "cic:/Coq/Arith/Lt/le_lt_trans.con". +alias id "le_plus_trans" = "cic:/Coq/Arith/Plus/le_plus_trans.con". +alias id "lt_le_trans" = "cic:/Coq/Arith/Lt/lt_le_trans.con". +alias id "lt_n_Sn" = "cic:/Coq/Arith/Lt/lt_n_Sn.con". +alias id "lt_S_n" = "cic:/Coq/Arith/Lt/lt_S_n.con". +alias id "lt_trans" = "cic:/Coq/Arith/Lt/lt_trans.con". +alias id "lt_wf_ind" = "cic:/Coq/Arith/Wf_nat/lt_wf_ind.con". +alias id "minus_n_n" = "cic:/Coq/Arith/Minus/minus_n_n.con". +alias id "minus_Sn_m" = "cic:/Coq/Arith/Minus/minus_Sn_m.con". +alias id "plus_le_lt_compat" = "cic:/Coq/Arith/Plus/plus_le_lt_compat.con". +alias id "plus_lt_compat" = "cic:/Coq/Arith/Plus/plus_lt_compat.con". +alias id "plus_lt_compat_r" = "cic:/Coq/Arith/Plus/plus_lt_compat_r.con". +alias id "plus_lt_le_compat" = "cic:/Coq/Arith/Plus/plus_lt_le_compat.con". +alias id "plus_n_O" = "cic:/Coq/Init/Peano/plus_n_O.con". +alias id "plus_Snm_nSm" = "cic:/Coq/Arith/Plus/plus_Snm_nSm.con". +alias id "S_pred" = "cic:/Coq/Arith/Lt/S_pred.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/spare.ma deleted file mode 100644 index 70b94347b..000000000 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare.ma +++ /dev/null @@ -1,118 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/spare". - -include "theory.ma". - -inductive sort: T \to Prop \def -| sort_sort: \forall (n: nat).(sort (TSort n)) -| sort_abst: \forall (u: T).((sort u) \to (\forall (t: T).((sort t) \to (sort -(THead (Bind Abst) u t))))). - -theorem sort_nf2: - \forall (t: T).((sort t) \to (\forall (c: C).(nf2 c t))) -\def - \lambda (t: T).(\lambda (H: (sort t)).(sort_ind (\lambda (t0: T).(\forall -(c: C).(nf2 c t0))) (\lambda (n: nat).(\lambda (c: C).(nf2_sort c n))) -(\lambda (u: T).(\lambda (_: (sort u)).(\lambda (H1: ((\forall (c: C).(nf2 c -u)))).(\lambda (t0: T).(\lambda (_: (sort t0)).(\lambda (H3: ((\forall (c: -C).(nf2 c t0)))).(\lambda (c: C).(let H_y \def (H3 (CHead c (Bind Abst) u)) -in (nf2_abst_shift c u (H1 c) t0 H_y))))))))) t H)). - -theorem sort_pc3: - \forall (t1: T).((sort t1) \to (\forall (t2: T).((sort t2) \to (\forall (c: -C).((pc3 c t1 t2) \to (eq T t1 t2)))))) -\def - \lambda (t1: T).(\lambda (H: (sort t1)).(sort_ind (\lambda (t: T).(\forall -(t2: T).((sort t2) \to (\forall (c: C).((pc3 c t t2) \to (eq T t t2)))))) -(\lambda (n: nat).(\lambda (t2: T).(\lambda (H0: (sort t2)).(sort_ind -(\lambda (t: T).(\forall (c: C).((pc3 c (TSort n) t) \to (eq T (TSort n) -t)))) (\lambda (n0: nat).(\lambda (c: C).(\lambda (H1: (pc3 c (TSort n) -(TSort n0))).(eq_ind nat n (\lambda (n1: nat).(eq T (TSort n) (TSort n1))) -(refl_equal T (TSort n)) n0 (pc3_gen_sort c n n0 H1))))) (\lambda (u: -T).(\lambda (_: (sort u)).(\lambda (_: ((\forall (c: C).((pc3 c (TSort n) u) -\to (eq T (TSort n) u))))).(\lambda (t: T).(\lambda (_: (sort t)).(\lambda -(_: ((\forall (c: C).((pc3 c (TSort n) t) \to (eq T (TSort n) t))))).(\lambda -(c: C).(\lambda (H5: (pc3 c (TSort n) (THead (Bind Abst) u -t))).(pc3_gen_sort_abst c u t n H5 (eq T (TSort n) (THead (Bind Abst) u -t))))))))))) t2 H0)))) (\lambda (u: T).(\lambda (_: (sort u)).(\lambda (H1: -((\forall (t2: T).((sort t2) \to (\forall (c: C).((pc3 c u t2) \to (eq T u -t2))))))).(\lambda (t: T).(\lambda (_: (sort t)).(\lambda (H3: ((\forall (t2: -T).((sort t2) \to (\forall (c: C).((pc3 c t t2) \to (eq T t -t2))))))).(\lambda (t2: T).(\lambda (H4: (sort t2)).(sort_ind (\lambda (t0: -T).(\forall (c: C).((pc3 c (THead (Bind Abst) u t) t0) \to (eq T (THead (Bind -Abst) u t) t0)))) (\lambda (n: nat).(\lambda (c: C).(\lambda (H5: (pc3 c -(THead (Bind Abst) u t) (TSort n))).(pc3_gen_sort_abst c u t n (pc3_s c -(TSort n) (THead (Bind Abst) u t) H5) (eq T (THead (Bind Abst) u t) (TSort -n)))))) (\lambda (u0: T).(\lambda (H5: (sort u0)).(\lambda (_: ((\forall (c: -C).((pc3 c (THead (Bind Abst) u t) u0) \to (eq T (THead (Bind Abst) u t) -u0))))).(\lambda (t0: T).(\lambda (H7: (sort t0)).(\lambda (_: ((\forall (c: -C).((pc3 c (THead (Bind Abst) u t) t0) \to (eq T (THead (Bind Abst) u t) -t0))))).(\lambda (c: C).(\lambda (H9: (pc3 c (THead (Bind Abst) u t) (THead -(Bind Abst) u0 t0))).(and_ind (pc3 c u u0) (\forall (b: B).(\forall (u1: -T).(pc3 (CHead c (Bind b) u1) t t0))) (eq T (THead (Bind Abst) u t) (THead -(Bind Abst) u0 t0)) (\lambda (H10: (pc3 c u u0)).(\lambda (H11: ((\forall (b: -B).(\forall (u1: T).(pc3 (CHead c (Bind b) u1) t t0))))).(let H_y \def (H11 -Abbr u) in (let H_y0 \def (H1 u0 H5 c H10) in (let H_y1 \def (H3 t0 H7 (CHead -c (Bind Abbr) u) H_y) in (let H12 \def (eq_ind_r T t0 (\lambda (t3: T).(pc3 -(CHead c (Bind Abbr) u) t t3)) H_y t H_y1) in (let H13 \def (eq_ind_r T t0 -(\lambda (t3: T).(sort t3)) H7 t H_y1) in (eq_ind T t (\lambda (t3: T).(eq T -(THead (Bind Abst) u t) (THead (Bind Abst) u0 t3))) (let H14 \def (eq_ind_r T -u0 (\lambda (t3: T).(pc3 c u t3)) H10 u H_y0) in (let H15 \def (eq_ind_r T u0 -(\lambda (t3: T).(sort t3)) H5 u H_y0) in (eq_ind T u (\lambda (t3: T).(eq T -(THead (Bind Abst) u t) (THead (Bind Abst) t3 t))) (refl_equal T (THead (Bind -Abst) u t)) u0 H_y0))) t0 H_y1)))))))) (pc3_gen_abst c u u0 t t0 H9)))))))))) -t2 H4))))))))) t1 H)). - -theorem sort_correct: - \forall (g: G).(\forall (t1: T).((sort t1) \to (\forall (c: C).(ex3 T -(\lambda (t2: T).(tau0 g c t1 t2)) (\lambda (t2: T).(ty3 g c t1 t2)) (\lambda -(t2: T).(sort t2)))))) -\def - \lambda (g: G).(\lambda (t1: T).(\lambda (H: (sort t1)).(sort_ind (\lambda -(t: T).(\forall (c: C).(ex3 T (\lambda (t2: T).(tau0 g c t t2)) (\lambda (t2: -T).(ty3 g c t t2)) (\lambda (t2: T).(sort t2))))) (\lambda (n: nat).(\lambda -(c: C).(ex3_intro T (\lambda (t2: T).(tau0 g c (TSort n) t2)) (\lambda (t2: -T).(ty3 g c (TSort n) t2)) (\lambda (t2: T).(sort t2)) (TSort (next g n)) -(tau0_sort g c n) (ty3_sort g c n) (sort_sort (next g n))))) (\lambda (u: -T).(\lambda (H0: (sort u)).(\lambda (H1: ((\forall (c: C).(ex3 T (\lambda -(t2: T).(tau0 g c u t2)) (\lambda (t2: T).(ty3 g c u t2)) (\lambda (t2: -T).(sort t2)))))).(\lambda (t: T).(\lambda (_: (sort t)).(\lambda (H3: -((\forall (c: C).(ex3 T (\lambda (t2: T).(tau0 g c t t2)) (\lambda (t2: -T).(ty3 g c t t2)) (\lambda (t2: T).(sort t2)))))).(\lambda (c: C).(let H_x -\def (H1 c) in (let H4 \def H_x in (ex3_ind T (\lambda (t2: T).(tau0 g c u -t2)) (\lambda (t2: T).(ty3 g c u t2)) (\lambda (t2: T).(sort t2)) (ex3 T -(\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(ty3 -g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort t2))) (\lambda (x0: -T).(\lambda (_: (tau0 g c u x0)).(\lambda (H6: (ty3 g c u x0)).(\lambda (_: -(sort x0)).(let H_x0 \def (H3 (CHead c (Bind Abst) u)) in (let H8 \def H_x0 -in (ex3_ind T (\lambda (t2: T).(tau0 g (CHead c (Bind Abst) u) t t2)) -(\lambda (t2: T).(ty3 g (CHead c (Bind Abst) u) t t2)) (\lambda (t2: T).(sort -t2)) (ex3 T (\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2)) (\lambda -(t2: T).(ty3 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort t2))) -(\lambda (x1: T).(\lambda (H9: (tau0 g (CHead c (Bind Abst) u) t -x1)).(\lambda (H10: (ty3 g (CHead c (Bind Abst) u) t x1)).(\lambda (H11: -(sort x1)).(ex_ind T (\lambda (t0: T).(ty3 g (CHead c (Bind Abst) u) x1 t0)) -(ex3 T (\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: -T).(ty3 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort t2))) -(\lambda (x: T).(\lambda (H12: (ty3 g (CHead c (Bind Abst) u) x1 -x)).(ex3_intro T (\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2)) -(\lambda (t2: T).(ty3 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort -t2)) (THead (Bind Abst) u x1) (tau0_bind g Abst c u t x1 H9) (ty3_bind g c u -x0 H6 Abst t x1 H10 x H12) (sort_abst u H0 x1 H11)))) (ty3_correct g (CHead c -(Bind Abst) u) t x1 H10)))))) H8))))))) H4)))))))))) t1 H))). - diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare3.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare3.ma new file mode 100644 index 000000000..891665097 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare3.ma @@ -0,0 +1,118 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + + + +include "theory.ma". + +inductive sort: T \to Prop \def +| sort_sort: \forall (n: nat).(sort (TSort n)) +| sort_abst: \forall (u: T).((sort u) \to (\forall (t: T).((sort t) \to (sort +(THead (Bind Abst) u t))))). + +theorem sort_nf2: + \forall (t: T).((sort t) \to (\forall (c: C).(nf2 c t))) +\def + \lambda (t: T).(\lambda (H: (sort t)).(sort_ind (\lambda (t0: T).(\forall +(c: C).(nf2 c t0))) (\lambda (n: nat).(\lambda (c: C).(nf2_sort c n))) +(\lambda (u: T).(\lambda (_: (sort u)).(\lambda (H1: ((\forall (c: C).(nf2 c +u)))).(\lambda (t0: T).(\lambda (_: (sort t0)).(\lambda (H3: ((\forall (c: +C).(nf2 c t0)))).(\lambda (c: C).(let H_y \def (H3 (CHead c (Bind Abst) u)) +in (nf2_abst_shift c u (H1 c) t0 H_y))))))))) t H)). + +theorem sort_pc3: + \forall (t1: T).((sort t1) \to (\forall (t2: T).((sort t2) \to (\forall (c: +C).((pc3 c t1 t2) \to (eq T t1 t2)))))) +\def + \lambda (t1: T).(\lambda (H: (sort t1)).(sort_ind (\lambda (t: T).(\forall +(t2: T).((sort t2) \to (\forall (c: C).((pc3 c t t2) \to (eq T t t2)))))) +(\lambda (n: nat).(\lambda (t2: T).(\lambda (H0: (sort t2)).(sort_ind +(\lambda (t: T).(\forall (c: C).((pc3 c (TSort n) t) \to (eq T (TSort n) +t)))) (\lambda (n0: nat).(\lambda (c: C).(\lambda (H1: (pc3 c (TSort n) +(TSort n0))).(eq_ind nat n (\lambda (n1: nat).(eq T (TSort n) (TSort n1))) +(refl_equal T (TSort n)) n0 (pc3_gen_sort c n n0 H1))))) (\lambda (u: +T).(\lambda (_: (sort u)).(\lambda (_: ((\forall (c: C).((pc3 c (TSort n) u) +\to (eq T (TSort n) u))))).(\lambda (t: T).(\lambda (_: (sort t)).(\lambda +(_: ((\forall (c: C).((pc3 c (TSort n) t) \to (eq T (TSort n) t))))).(\lambda +(c: C).(\lambda (H5: (pc3 c (TSort n) (THead (Bind Abst) u +t))).(pc3_gen_sort_abst c u t n H5 (eq T (TSort n) (THead (Bind Abst) u +t))))))))))) t2 H0)))) (\lambda (u: T).(\lambda (_: (sort u)).(\lambda (H1: +((\forall (t2: T).((sort t2) \to (\forall (c: C).((pc3 c u t2) \to (eq T u +t2))))))).(\lambda (t: T).(\lambda (_: (sort t)).(\lambda (H3: ((\forall (t2: +T).((sort t2) \to (\forall (c: C).((pc3 c t t2) \to (eq T t +t2))))))).(\lambda (t2: T).(\lambda (H4: (sort t2)).(sort_ind (\lambda (t0: +T).(\forall (c: C).((pc3 c (THead (Bind Abst) u t) t0) \to (eq T (THead (Bind +Abst) u t) t0)))) (\lambda (n: nat).(\lambda (c: C).(\lambda (H5: (pc3 c +(THead (Bind Abst) u t) (TSort n))).(pc3_gen_sort_abst c u t n (pc3_s c +(TSort n) (THead (Bind Abst) u t) H5) (eq T (THead (Bind Abst) u t) (TSort +n)))))) (\lambda (u0: T).(\lambda (H5: (sort u0)).(\lambda (_: ((\forall (c: +C).((pc3 c (THead (Bind Abst) u t) u0) \to (eq T (THead (Bind Abst) u t) +u0))))).(\lambda (t0: T).(\lambda (H7: (sort t0)).(\lambda (_: ((\forall (c: +C).((pc3 c (THead (Bind Abst) u t) t0) \to (eq T (THead (Bind Abst) u t) +t0))))).(\lambda (c: C).(\lambda (H9: (pc3 c (THead (Bind Abst) u t) (THead +(Bind Abst) u0 t0))).(and_ind (pc3 c u u0) (\forall (b: B).(\forall (u1: +T).(pc3 (CHead c (Bind b) u1) t t0))) (eq T (THead (Bind Abst) u t) (THead +(Bind Abst) u0 t0)) (\lambda (H10: (pc3 c u u0)).(\lambda (H11: ((\forall (b: +B).(\forall (u1: T).(pc3 (CHead c (Bind b) u1) t t0))))).(let H_y \def (H11 +Abbr u) in (let H_y0 \def (H1 u0 H5 c H10) in (let H_y1 \def (H3 t0 H7 (CHead +c (Bind Abbr) u) H_y) in (let H12 \def (eq_ind_r T t0 (\lambda (t3: T).(pc3 +(CHead c (Bind Abbr) u) t t3)) H_y t H_y1) in (let H13 \def (eq_ind_r T t0 +(\lambda (t3: T).(sort t3)) H7 t H_y1) in (eq_ind T t (\lambda (t3: T).(eq T +(THead (Bind Abst) u t) (THead (Bind Abst) u0 t3))) (let H14 \def (eq_ind_r T +u0 (\lambda (t3: T).(pc3 c u t3)) H10 u H_y0) in (let H15 \def (eq_ind_r T u0 +(\lambda (t3: T).(sort t3)) H5 u H_y0) in (eq_ind T u (\lambda (t3: T).(eq T +(THead (Bind Abst) u t) (THead (Bind Abst) t3 t))) (refl_equal T (THead (Bind +Abst) u t)) u0 H_y0))) t0 H_y1)))))))) (pc3_gen_abst c u u0 t t0 H9)))))))))) +t2 H4))))))))) t1 H)). + +theorem sort_correct: + \forall (g: G).(\forall (t1: T).((sort t1) \to (\forall (c: C).(ex3 T +(\lambda (t2: T).(tau0 g c t1 t2)) (\lambda (t2: T).(ty3 g c t1 t2)) (\lambda +(t2: T).(sort t2)))))) +\def + \lambda (g: G).(\lambda (t1: T).(\lambda (H: (sort t1)).(sort_ind (\lambda +(t: T).(\forall (c: C).(ex3 T (\lambda (t2: T).(tau0 g c t t2)) (\lambda (t2: +T).(ty3 g c t t2)) (\lambda (t2: T).(sort t2))))) (\lambda (n: nat).(\lambda +(c: C).(ex3_intro T (\lambda (t2: T).(tau0 g c (TSort n) t2)) (\lambda (t2: +T).(ty3 g c (TSort n) t2)) (\lambda (t2: T).(sort t2)) (TSort (next g n)) +(tau0_sort g c n) (ty3_sort g c n) (sort_sort (next g n))))) (\lambda (u: +T).(\lambda (H0: (sort u)).(\lambda (H1: ((\forall (c: C).(ex3 T (\lambda +(t2: T).(tau0 g c u t2)) (\lambda (t2: T).(ty3 g c u t2)) (\lambda (t2: +T).(sort t2)))))).(\lambda (t: T).(\lambda (_: (sort t)).(\lambda (H3: +((\forall (c: C).(ex3 T (\lambda (t2: T).(tau0 g c t t2)) (\lambda (t2: +T).(ty3 g c t t2)) (\lambda (t2: T).(sort t2)))))).(\lambda (c: C).(let H_x +\def (H1 c) in (let H4 \def H_x in (ex3_ind T (\lambda (t2: T).(tau0 g c u +t2)) (\lambda (t2: T).(ty3 g c u t2)) (\lambda (t2: T).(sort t2)) (ex3 T +(\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(ty3 +g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort t2))) (\lambda (x0: +T).(\lambda (_: (tau0 g c u x0)).(\lambda (H6: (ty3 g c u x0)).(\lambda (_: +(sort x0)).(let H_x0 \def (H3 (CHead c (Bind Abst) u)) in (let H8 \def H_x0 +in (ex3_ind T (\lambda (t2: T).(tau0 g (CHead c (Bind Abst) u) t t2)) +(\lambda (t2: T).(ty3 g (CHead c (Bind Abst) u) t t2)) (\lambda (t2: T).(sort +t2)) (ex3 T (\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2)) (\lambda +(t2: T).(ty3 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort t2))) +(\lambda (x1: T).(\lambda (H9: (tau0 g (CHead c (Bind Abst) u) t +x1)).(\lambda (H10: (ty3 g (CHead c (Bind Abst) u) t x1)).(\lambda (H11: +(sort x1)).(ex_ind T (\lambda (t0: T).(ty3 g (CHead c (Bind Abst) u) x1 t0)) +(ex3 T (\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: +T).(ty3 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort t2))) +(\lambda (x: T).(\lambda (H12: (ty3 g (CHead c (Bind Abst) u) x1 +x)).(ex3_intro T (\lambda (t2: T).(tau0 g c (THead (Bind Abst) u t) t2)) +(\lambda (t2: T).(ty3 g c (THead (Bind Abst) u t) t2)) (\lambda (t2: T).(sort +t2)) (THead (Bind Abst) u x1) (tau0_bind g Abst c u t x1 H9) (ty3_bind g c u +x0 H6 Abst t x1 H10 x H12) (sort_abst u H0 x1 H11)))) (ty3_correct g (CHead c +(Bind Abst) u) t x1 H10)))))) H8))))))) H4)))))))))) t1 H))). + 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/theory.ma deleted file mode 100644 index daf2a250e..000000000 --- a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma +++ /dev/null @@ -1,38 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -(* This file was automatically generated: do not edit *********************) - -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/theory". - -include "subst0/tlt.ma". - -include "tau1/cnt.ma". - -include "ex0/props.ma". - -include "wcpr0/fwd.ma". - -include "pr3/wcpr0.ma". - -include "ex2/props.ma". - -include "ex1/props.ma". - -include "ty3/tau0.ma". - -include "ty3/nf2.ma". - -include "ty3/dec.ma". - diff --git a/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory3.ma b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory3.ma new file mode 100644 index 000000000..b0d977422 --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory3.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* This file was automatically generated: do not edit *********************) + + + +include "subst0/tlt.ma". + +include "tau1/cnt.ma". + +include "ex0/props.ma". + +include "wcpr0/fwd.ma". + +include "pr3/wcpr0.ma". + +include "ex2/props.ma". + +include "ex1/props.ma". + +include "ty3/tau0.ma". + +include "ty3/nf2.ma". + +include "ty3/dec.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/preamble.ma deleted file mode 100644 index d889c3995..000000000 --- a/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble.ma +++ /dev/null @@ -1,34 +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 *) -(* *) -(**************************************************************************) - -(* 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". - -axiom f_equal_3: \forall (A,B,C,D:Set). - \forall (f:A \to B \to C \to D). - \forall (x1,x2:A). - \forall (y1,y2:B). - \forall (z1,z2:C). - x1 = x2 \to y1 = y2 \to z1 = z2 \to - f x1 y1 z1 = f x2 y2 z2. diff --git a/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble4.ma b/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble4.ma new file mode 100644 index 000000000..1449c154f --- /dev/null +++ b/matita/contribs/LAMBDA-TYPES/Unified-Sub/preamble4.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* Project started Tue Aug 22, 2006 ***************************************) + + + +(* PREAMBLE +*) + +include "logic/equality.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). + \forall (x1,x2:A). + \forall (y1,y2:B). + \forall (z1,z2:C). + x1 = x2 \to y1 = y2 \to z1 = z2 \to + f x1 y1 z1 = f x2 y2 z2. 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 - ] -*)