From d0982534aee06a30f91a06d2f3e82834b132a3d3 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 13 Feb 2008 17:56:43 +0000 Subject: [PATCH] baseuris removed from files --- helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/defs.ma | 2 -- helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/props.ma | 2 -- .../software/matita/contribs/LAMBDA-TYPES/Base-1/definitions.ma | 2 -- helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma | 2 -- .../software/matita/contribs/LAMBDA-TYPES/Base-1/ext/tactics.ma | 2 -- helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/defs.ma | 2 -- .../software/matita/contribs/LAMBDA-TYPES/Base-1/plist/props.ma | 2 -- helm/software/matita/contribs/LAMBDA-TYPES/Base-1/spare.ma | 2 -- helm/software/matita/contribs/LAMBDA-TYPES/Base-1/theory.ma | 2 -- helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma | 2 -- .../software/matita/contribs/LAMBDA-TYPES/Base-1/types/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/A/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/G/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/dec.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/aprem.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/cimp.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/lift1.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/pr3.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/subst0.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/drop.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/getl.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/arity.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/clear.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/drop.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/getl.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/arity.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/clear.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/csuba.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop1.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/getl.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/clear.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/drop.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/getl.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/getl.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/clear.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/drop.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/getl.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/pc3.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/getl.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/clear.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/dec.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/drop.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/flt.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/getl.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/asucc.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/props.ma | 2 -- .../contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/defs.ma | 2 -- .../contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/arity.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/dec.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/iso.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/lift1.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/pr3.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/dec.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fsubst0.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/left.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/nf2.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/pc1.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/subst1.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/wcpr0.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/dec.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/subst1.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/pr1.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/clen.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/pr2.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/iso.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr1.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr3.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/subst1.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/wcpr0.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/arity.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/lift1.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/nf2.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/dec.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/subst0.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/subst1.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/cnt.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity.ma | 2 -- .../contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/dec.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/defs.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/fwd.ma | 2 -- .../matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/getl.ma | 2 -- 209 files changed, 418 deletions(-) diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/defs.ma index 4864a2c86..293c184f5 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/blt/defs". - include "preamble.ma". definition blt: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/props.ma index ea4d32b2b..3cff54f96 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/blt/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/blt/props". - include "blt/defs.ma". theorem lt_blt: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/definitions.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/definitions.ma index ec3212d25..3a087dec7 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/definitions.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/definitions.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/definitions". - include "types/defs.ma". include "blt/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma index 908a0df78..70a94bfbd 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/arith.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/ext/arith". - include "preamble.ma". theorem nat_dec: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/tactics.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/tactics.ma index 09f9fa05f..7fcdc28ec 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/tactics.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/ext/tactics.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/ext/tactics". - include "preamble.ma". theorem insert_eq: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/defs.ma index 1ca1142d9..9cfca05ae 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/plist/defs". - include "preamble.ma". inductive PList: Set \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/props.ma index 7338262f1..bc480cc23 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/plist/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/plist/props". - include "plist/defs.ma". theorem papp_ss: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/spare.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/spare.ma index f66934f78..c62e67982 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/spare.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/spare.ma @@ -14,7 +14,5 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/spare". - include "theory.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/theory.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/theory.ma index d89a21858..c7c94ce53 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/theory.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/theory.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/theory". - include "ext/tactics.ma". include "ext/arith.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma index bc874fb08..cb8300ade 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/types/defs". - include "preamble.ma". inductive and3 (P0: Prop) (P1: Prop) (P2: Prop): Prop \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/props.ma index 1c9b499bb..b27665600 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-1/types/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-1/types/props". - include "types/defs.ma". theorem ex2_sym: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/A/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/A/defs.ma index 1c592efd2..1c5def44f 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/A/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/A/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/A/defs". - include "preamble.ma". inductive A: Set \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/defs.ma index 0022395ce..042be1801 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/C/defs". - include "T/defs.ma". inductive C: Set \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/props.ma index 30901423e..06252c222 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/C/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/C/props". - include "C/defs.ma". include "T/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/G/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/G/defs.ma index d66873d06..dbc7f7ad2 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/G/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/G/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/G/defs". - include "preamble.ma". record G : Set \def { diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/dec.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/dec.ma index 0d05ba97f..044e04557 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/dec.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/dec.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/dec". - include "T/defs.ma". theorem terms_props__bind_dec: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/defs.ma index 236063dcf..951e1b920 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs". - include "preamble.ma". inductive B: Set \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/props.ma index 1c661524e..2fb7361a1 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/T/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/props". - include "T/defs.ma". theorem not_abbr_abst: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/defs.ma index 0a1c35ea2..98f15dde2 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/aplus/defs". - include "asucc/defs.ma". definition aplus: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/props.ma index 16adef5c3..e0b2bcaca 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aplus/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/aplus/props". - include "aplus/defs.ma". include "next_plus/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/defs.ma index 258037275..bcc17b031 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/aprem/defs". - include "A/defs.ma". inductive aprem: nat \to (A \to (A \to Prop)) \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/props.ma index 60264bca2..0c38f1e49 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/aprem/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/aprem/props". - include "aprem/defs.ma". include "leq/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/aprem.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/aprem.ma index e3a36f11c..9aef2e8a0 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/aprem.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/aprem.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/aprem". - include "arity/props.ma". include "arity/cimp.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/cimp.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/cimp.ma index 2af721d15..dbe488b0e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/cimp.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/cimp.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/cimp". - include "arity/defs.ma". include "cimp/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/defs.ma index 410400d5f..5d2979dc4 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/defs". - include "leq/defs.ma". include "getl/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma index 0c8151174..fe241d0dc 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/fwd". - include "arity/defs.ma". include "leq/asucc.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/lift1.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/lift1.ma index 46e4c8c86..c6270d035 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/lift1.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/lift1.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/lift1". - include "arity/props.ma". include "drop1/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/pr3.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/pr3.ma index 67617b31a..15697c87d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/pr3.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/pr3.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/pr3". - include "csuba/arity.ma". include "pr3/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/props.ma index 6c9662aeb..301c26c6c 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/props". - include "arity/fwd.ma". theorem node_inh: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/subst0.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/subst0.ma index 4592f394a..d3f4f1373 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/subst0.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/arity/subst0.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/arity/subst0". - include "arity/props.ma". include "fsubst0/fwd.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/defs.ma index ae2233051..9dfd88b80 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/asucc/defs". - include "A/defs.ma". include "G/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/fwd.ma index d2c77132e..0093edc25 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/asucc/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/asucc/fwd". - include "asucc/defs.ma". theorem asucc_gen_sort: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/defs.ma index c5390f97b..3182b1231 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/cimp/defs". - include "getl/defs.ma". definition cimp: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/props.ma index ae0f6a567..f8baf8cae 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cimp/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/cimp/props". - include "cimp/defs.ma". include "getl/getl.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/defs.ma index 118dc7ccf..39deb2fe5 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clear/defs". - include "C/defs.ma". inductive clear: C \to (C \to Prop) \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/drop.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/drop.ma index 2cfcaa874..07fb8137b 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/drop.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/drop.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clear/drop". - include "clear/fwd.ma". include "drop/fwd.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/fwd.ma index fe23589d5..bec178d77 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clear/fwd". - include "clear/defs.ma". theorem clear_gen_sort: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/props.ma index a1880711d..6a99a80d7 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clear/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clear/props". - include "clear/fwd.ma". theorem clear_clear: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/defs.ma index 2885518ea..a17a17307 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clen/defs". - include "C/defs.ma". include "s/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/getl.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/getl.ma index 8773297ca..dcfb3d8bb 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/getl.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/clen/getl.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/clen/getl". - include "clen/defs.ma". include "getl/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/defs.ma index f9b4334e1..a1e32c285 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/cnt/defs". - include "T/defs.ma". inductive cnt: T \to Prop \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/props.ma index 81620ce9e..9d4c19f9f 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/cnt/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/cnt/props". - include "cnt/defs.ma". include "lift/fwd.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/arity.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/arity.ma index ff9d01c9e..9b4f9d222 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/arity.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/arity.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/arity". - include "csuba/getl.ma". include "csuba/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/clear.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/clear.ma index 036ca2882..3a21edd7d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/clear.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/clear.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/clear". - include "csuba/defs.ma". include "clear/fwd.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/defs.ma index 1b8612a2f..5b1bb92c3 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/defs". - include "arity/defs.ma". inductive csuba (g: G): C \to (C \to Prop) \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/drop.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/drop.ma index 003b18a5e..4d965603c 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/drop.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/drop.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/drop". - include "csuba/fwd.ma". include "drop/fwd.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/fwd.ma index 2b56bc7a0..6a34ae7e7 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/fwd". - include "csuba/defs.ma". theorem csuba_gen_abbr: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/getl.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/getl.ma index d93e4d618..f75cc859a 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/getl.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/getl.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/getl". - include "csuba/drop.ma". include "csuba/clear.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/props.ma index 62e10c095..c92cb5301 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csuba/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csuba/props". - include "csuba/defs.ma". theorem csuba_refl: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/arity.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/arity.ma index d697f1257..003658f0e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/arity.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/arity.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/arity". - include "csubc/csuba.ma". include "arity/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/clear.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/clear.ma index 059c359ab..a386ad644 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/clear.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/clear.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/clear". - include "csubc/defs.ma". theorem csubc_clear_conf: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/csuba.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/csuba.ma index 646247a79..49c062fd1 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/csuba.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/csuba.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/csuba". - include "csubc/defs.ma". include "sc3/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/defs.ma index 6348a632b..bfe52dc36 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/defs". - include "sc3/defs.ma". inductive csubc (g: G): C \to (C \to Prop) \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop.ma index 301cba935..4a0803636 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/drop". - include "csubc/defs.ma". include "sc3/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop1.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop1.ma index 75651a172..a1f8cbb64 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop1.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/drop1.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/drop1". - include "csubc/drop.ma". theorem drop1_csubc_trans: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/getl.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/getl.ma index dd2a0397c..4ab71a145 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/getl.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/getl.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/getl". - include "csubc/drop.ma". include "csubc/clear.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/props.ma index d13d2b09f..17e95182b 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubc/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubc/props". - include "csubc/defs.ma". include "sc3/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/clear.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/clear.ma index fb9fdf5a5..0ecdcc1cf 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/clear.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/clear.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/clear". - include "csubst0/fwd.ma". include "clear/fwd.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/defs.ma index 5d90ea599..3b26bb371 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/defs". - include "subst0/defs.ma". include "C/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/drop.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/drop.ma index 814c2eb1e..c3e86929e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/drop.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/drop.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/drop". - include "csubst0/fwd.ma". include "drop/fwd.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/fwd.ma index 7980be5fc..31854f925 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/fwd". - include "csubst0/defs.ma". theorem csubst0_gen_sort: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/getl.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/getl.ma index d4ccb6ee5..e724aa55d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/getl.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/getl.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/getl". - include "csubst0/clear.ma". include "csubst0/drop.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/props.ma index 24e20c400..527cc5bb8 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst0/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst0/props". - include "csubst0/defs.ma". theorem csubst0_snd_bind: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/defs.ma index a298dfc8c..0684e35b6 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst1/defs". - include "csubst0/defs.ma". inductive csubst1 (i: nat) (v: T) (c1: C): C \to Prop \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/fwd.ma index 96e86eea5..60f422c5c 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst1/fwd". - include "csubst1/defs.ma". include "csubst0/fwd.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/getl.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/getl.ma index a6af74625..960f16d78 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/getl.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/getl.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst1/getl". - include "csubst1/props.ma". include "csubst0/getl.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/props.ma index 9cafa826f..0a73f8d22 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubst1/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubst1/props". - include "csubst1/defs.ma". include "subst1/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/clear.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/clear.ma index 22581895b..6a6c2ec62 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/clear.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/clear.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/clear". - include "csubt/defs.ma". include "clear/fwd.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/defs.ma index 3f90ff3ce..6627d5eff 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/defs". - include "ty3/defs.ma". inductive csubt (g: G): C \to (C \to Prop) \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/drop.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/drop.ma index 7a7efe4ce..8c834e611 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/drop.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/drop.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/drop". - include "csubt/defs.ma". include "drop/fwd.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/fwd.ma index 92e19a503..1aac67dff 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/fwd". - include "csubt/defs.ma". theorem csubt_inv_coq: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/getl.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/getl.ma index a0f89e0fa..1f39ef182 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/getl.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/getl.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/getl". - include "csubt/fwd.ma". include "csubt/clear.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/pc3.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/pc3.ma index d8a6ad246..342443cf6 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/pc3.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/pc3.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/pc3". - include "csubt/getl.ma". include "pc3/left.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/props.ma index 5d88520a9..766ba4589 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/props". - include "csubt/defs.ma". theorem csubt_refl: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3.ma index 82bd40a5c..cc8839f26 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/csubt/ty3". - include "csubt/pc3.ma". include "csubt/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions.ma index 620154782..7b6e09292 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/definitions.ma @@ -14,8 +14,6 @@ (* 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". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/defs.ma index e0b46886f..8967b8645 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop/defs". - include "C/defs.ma". include "lift/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/fwd.ma index ed0d67636..b4653f80f 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop/fwd". - include "drop/defs.ma". theorem drop_gen_sort: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/props.ma index 029720727..39343a178 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop/props". - include "drop/fwd.ma". include "lift/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/defs.ma index dea03ca70..78e13d219 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop1/defs". - include "drop/defs.ma". include "lift1/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/getl.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/getl.ma index f8ec287e3..711735acd 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/getl.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/getl.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop1/getl". - include "drop1/defs.ma". include "getl/drop.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/props.ma index 5d1e9dc29..1f6599d96 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/drop1/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/drop1/props". - include "drop1/defs.ma". include "drop/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/defs.ma index 078545c74..755b481e2 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex0/defs". - include "A/defs.ma". include "G/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/props.ma index 66350ed9c..c035c099e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex0/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex0/props". - include "ex0/defs.ma". include "leq/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/defs.ma index 3e16c05ed..e4e1e229d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex1/defs". - include "C/defs.ma". definition ex1_c: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma index 62d2ad59b..e809b11bf 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex1/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex1/props". - include "ex1/defs.ma". include "ty3/fwd.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/defs.ma index 482249d5e..713a5aac9 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex2/defs". - include "C/defs.ma". definition ex2_c: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/props.ma index f35ee3579..afcdfbfe5 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ex2/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ex2/props". - include "ex2/defs.ma". include "nf2/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/defs.ma index 9143b89a2..020a79788 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/flt/defs". - include "C/defs.ma". definition fweight: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/props.ma index a8d7daff3..bdb5ccaa0 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/flt/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/flt/props". - include "flt/defs.ma". include "C/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/defs.ma index d3eccba43..9da21ae76 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/fsubst0/defs". - include "csubst0/defs.ma". include "subst0/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/fwd.ma index 773e57278..85696f0b3 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/fsubst0/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/fsubst0/fwd". - include "fsubst0/defs.ma". theorem fsubst0_gen_base: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/clear.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/clear.ma index 8b7c55259..22bbb7ec2 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/clear.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/clear.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/clear". - include "getl/props.ma". include "clear/drop.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/dec.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/dec.ma index f22b7b333..01ce28e0d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/dec.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/dec.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/dec". - include "getl/props.ma". theorem getl_dec: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/defs.ma index 0d97227a1..545b48953 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/defs". - include "drop/defs.ma". include "clear/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/drop.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/drop.ma index c176ca62d..47d5168a4 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/drop.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/drop.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/drop". - include "getl/props.ma". include "clear/drop.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/flt.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/flt.ma index 81a47ff2e..f4d4ffa8d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/flt.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/flt.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/flt". - include "getl/fwd.ma". include "clear/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/fwd.ma index 538165227..0f3244947 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/fwd". - include "getl/defs.ma". include "drop/fwd.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/getl.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/getl.ma index 62218d746..5534efff6 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/getl.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/getl.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/getl". - include "getl/drop.ma". include "getl/clear.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/props.ma index a5228d950..3c884173d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/getl/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/getl/props". - include "getl/fwd.ma". include "drop/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/defs.ma index fa327f922..58bf0424c 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/iso/defs". - include "T/defs.ma". inductive iso: T \to (T \to Prop) \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/fwd.ma index 5a6607941..37ddce3ed 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/iso/fwd". - include "iso/defs.ma". include "tlist/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/props.ma index edc9758a9..215f79c28 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/iso/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/iso/props". - include "iso/fwd.ma". theorem iso_refl: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/asucc.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/asucc.ma index 25f9dfd07..ef8360a02 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/asucc.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/asucc.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/leq/asucc". - include "leq/props.ma". include "aplus/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/defs.ma index d14a0e535..dad66914d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/leq/defs". - include "aplus/defs.ma". inductive leq (g: G): A \to (A \to Prop) \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/fwd.ma index 36c26579b..6b953558d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/leq/fwd". - include "leq/defs.ma". theorem leq_gen_sort: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/props.ma index 0ad16f9e7..f74c7e47a 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/leq/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/leq/props". - include "leq/defs.ma". include "aplus/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/defs.ma index 9a03fcd17..49d9a670d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift/defs". - include "T/defs.ma". include "tlist/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma index 5a80f43e6..07f801655 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift/fwd". - include "lift/defs.ma". theorem lift_sort: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma index 6a8cc0ac0..428146f30 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift/props". - include "tlist/defs.ma". include "lift/fwd.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma index 0e041d02d..4c728e102 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift/tlt.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift/tlt". - include "lift/fwd.ma". include "tlt/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/defs.ma index 4042efeee..691829e8e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift1/defs". - include "lift/defs.ma". definition trans: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/fwd.ma index bbdef6d1f..de9bcba64 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift1/fwd". - include "lift1/defs.ma". include "lift/fwd.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma index db5d76536..154fd00c8 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/lift1/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/lift1/props". - include "lift1/defs.ma". include "lift/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/defs.ma index 19ef14486..b4d60f377 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/llt/defs". - include "A/defs.ma". definition lweight: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/props.ma index d34488300..6cfc3ca11 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/llt/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/llt/props". - include "llt/defs.ma". include "leq/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/defs.ma index 1764e8610..f7650f16d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/next_plus/defs". - include "G/defs.ma". definition next_plus: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/props.ma index e0f2654ac..b8d9a45ac 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/next_plus/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/next_plus/props". - include "next_plus/defs.ma". theorem next_plus_assoc: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/arity.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/arity.ma index d67f67282..a57a60930 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/arity.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/arity.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/arity". - include "nf2/fwd.ma". include "arity/subst0.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/dec.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/dec.ma index d7aa80992..85113c01d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/dec.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/dec.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/dec". - include "nf2/defs.ma". include "pr2/clen.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/defs.ma index 23868ee8b..df65c39b9 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/defs". - include "pr2/defs.ma". definition nf2: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/fwd.ma index 5b705dbba..8f9151fb9 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/fwd". - include "nf2/defs.ma". include "pr2/clen.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/iso.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/iso.ma index 54b097c04..d57d48f52 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/iso.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/iso.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/iso". - include "nf2/pr3.ma". include "pr3/fwd.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/lift1.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/lift1.ma index 33c44778d..48c9ddaa2 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/lift1.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/lift1.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/lift1". - include "nf2/props.ma". include "drop1/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/pr3.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/pr3.ma index 2206469dc..9f52c0d19 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/pr3.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/pr3.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/pr3". - include "nf2/defs.ma". include "pr3/pr3.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma index 7dfefe203..05f2b77f1 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/nf2/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/nf2/props". - include "nf2/defs.ma". include "pr2/fwd.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/defs.ma index c81142f5d..efe04085a 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc1/defs". - include "pr1/defs.ma". definition pc1: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/props.ma index 0bd48d44c..caa38f0fc 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc1/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc1/props". - include "pc1/defs.ma". include "pr1/pr1.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/dec.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/dec.ma index 138142369..70a73062f 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/dec.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/dec.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/dec". - include "ty3/arity_props.ma". include "ty3/pr3.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/defs.ma index 91d5eaf8b..0a2712197 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/defs". - include "pr3/defs.ma". definition pc3: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fsubst0.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fsubst0.ma index 6ab7daf1c..610fa416e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fsubst0.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fsubst0.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/fsubst0". - include "pc3/left.ma". include "fsubst0/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fwd.ma index cd70ecf45..cf4fad72f 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/fwd". - include "pc3/props.ma". include "pr3/fwd.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/left.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/left.ma index 3a6db7706..08d060d4d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/left.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/left.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/left". - include "pc3/props.ma". theorem pc3_ind_left__pc3_left_pr3: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/nf2.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/nf2.ma index 41136207b..73ec672fb 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/nf2.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/nf2.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/nf2". - include "pc3/defs.ma". include "nf2/pr3.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/pc1.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/pc1.ma index 0893239e4..a85f348cb 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/pc1.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/pc1.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/pc1". - include "pc3/defs.ma". include "pc1/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/props.ma index 98a40de4e..2685fe355 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/props". - include "pc3/defs.ma". include "pr3/pr3.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/subst1.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/subst1.ma index 510b2d649..404f98150 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/subst1.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/subst1.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/subst1". - include "pc3/props.ma". include "pr3/subst1.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/wcpr0.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/wcpr0.ma index 5ed59a431..9d8e8dc11 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/wcpr0.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pc3/wcpr0.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/wcpr0". - include "pc3/props.ma". include "wcpr0/getl.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/dec.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/dec.ma index 26c4a21b6..81a24cd79 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/dec.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/dec.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/dec". - include "pr0/fwd.ma". include "subst0/dec.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/defs.ma index 4086f5beb..a0f6bb299 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/defs". - include "subst0/defs.ma". inductive pr0: T \to (T \to Prop) \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/fwd.ma index e73b8a048..fb106f9ce 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/fwd". - include "pr0/props.ma". theorem pr0_inv_coq: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0.ma index 59e04cef8..207570e19 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/pr0". - include "pr0/fwd.ma". include "lift/tlt.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/props.ma index 5e8396c47..c10df0103 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/props". - include "pr0/defs.ma". include "subst0/subst0.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/subst1.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/subst1.ma index 0aa55239f..c7efff402 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/subst1.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr0/subst1.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr0/subst1". - include "pr0/props.ma". include "subst1/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/defs.ma index 85540bde7..bfa5c9d32 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr1/defs". - include "pr0/defs.ma". inductive pr1: T \to (T \to Prop) \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/pr1.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/pr1.ma index 98a21a512..9b935f805 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/pr1.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/pr1.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr1/pr1". - include "pr1/props.ma". include "pr0/pr0.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/props.ma index 7840b3cd2..a5d606b06 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr1/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr1/props". - include "pr1/defs.ma". include "pr0/subst1.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/clen.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/clen.ma index 0638ca3f6..b935b2616 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/clen.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/clen.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/clen". - include "pr2/props.ma". include "clen/getl.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/defs.ma index 77932c984..d712689b2 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/defs". - include "pr0/defs.ma". include "getl/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd.ma index 848d216fa..b2f5dff45 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/fwd". - include "pr2/defs.ma". include "pr0/fwd.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/pr2.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/pr2.ma index 307d55398..ba7a54835 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/pr2.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/pr2.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/pr2". - include "pr2/defs.ma". include "pr0/pr0.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/props.ma index 0a434d39a..8b11644d3 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/props". - include "pr2/defs.ma". include "pr0/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1.ma index 27a0221d5..9d230c6b1 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr2/subst1". - include "pr2/defs.ma". include "pr0/subst1.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/defs.ma index 3baff8a16..cd26300e7 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/defs". - include "pr2/defs.ma". inductive pr3 (c: C): T \to (T \to Prop) \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/fwd.ma index 470a3523a..690ccfce3 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/fwd". - include "pr3/props.ma". include "pr2/fwd.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/iso.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/iso.ma index 07b35477e..9e3d88402 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/iso.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/iso.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/iso". - include "pr3/fwd.ma". include "iso/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr1.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr1.ma index 21344033e..872444dc8 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr1.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr1.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/pr1". - include "pr3/defs.ma". include "pr1/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr3.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr3.ma index c29781a0e..62e34c4ee 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr3.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/pr3.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/pr3". - include "pr3/props.ma". include "pr2/pr2.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/props.ma index c07efa64d..67607a1e2 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/props". - include "pr3/pr1.ma". include "pr2/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/subst1.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/subst1.ma index 4894993fc..83c8cb75c 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/subst1.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/subst1.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/subst1". - include "pr3/defs.ma". include "pr2/subst1.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/wcpr0.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/wcpr0.ma index dd20dae41..df905f39c 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/wcpr0.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/pr3/wcpr0.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pr3/wcpr0". - include "pr3/props.ma". include "wcpr0/getl.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/defs.ma index 005f3a107..83ae2b2d2 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/r/defs". - include "T/defs.ma". definition r: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/props.ma index 505d1e450..20ae7a5cf 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/r/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/r/props". - include "r/defs.ma". include "s/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/defs.ma index 6cb9d340f..dbbf0665c 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/s/defs". - include "T/defs.ma". definition s: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/props.ma index 7acdf612f..b4c556f30 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/s/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/s/props". - include "s/defs.ma". theorem s_S: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/arity.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/arity.ma index e7f13ac61..7258d8d1a 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/arity.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/arity.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sc3/arity". - include "csubc/arity.ma". include "csubc/getl.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/defs.ma index fd161f395..be8cda450 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sc3/defs". - include "sn3/defs.ma". include "arity/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/props.ma index c1d3787b8..79645a1fd 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sc3/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sc3/props". - include "sc3/defs.ma". include "sn3/lift1.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/defs.ma index 0d38de3a8..ddf14abc2 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sn3/defs". - include "pr3/defs.ma". inductive sn3 (c: C): T \to Prop \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/fwd.ma index d20baeb59..c9db131a1 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sn3/fwd". - include "sn3/defs.ma". include "pr3/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/lift1.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/lift1.ma index d84d094a2..44fb2ca8e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/lift1.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/lift1.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sn3/lift1". - include "sn3/props.ma". include "drop1/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/nf2.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/nf2.ma index 7b5c1d1bb..152088179 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/nf2.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/nf2.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sn3/nf2". - include "sn3/defs.ma". include "nf2/dec.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma index ec20b825f..afd3fdbc9 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/sn3/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/sn3/props". - include "sn3/nf2.ma". include "sn3/fwd.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare.ma index 69354b4e3..c79beed0b 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/spare.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/spare". - include "theory.ma". definition cbk: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/dec.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/dec.ma index cfa2bbe3f..bbdc36832 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/dec.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/dec.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/dec". - include "subst0/defs.ma". include "lift/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/defs.ma index c675bc6ab..63eececf3 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/defs". - include "lift/defs.ma". inductive subst0: nat \to (T \to (T \to (T \to Prop))) \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd.ma index e16f362b0..612a3261a 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/fwd". - include "subst0/defs.ma". include "lift/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma index 7b147c20e..c36cd597e 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/props". - include "subst0/fwd.ma". include "lift/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/subst0.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/subst0.ma index 9b9c0bb54..c8a35b3a3 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/subst0.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/subst0.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/subst0". - include "subst0/props.ma". theorem subst0_subst0: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt.ma index fd0ba2f0c..87c1fec52 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst0/tlt". - include "subst0/defs.ma". include "lift/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/defs.ma index 304adc590..62cfc2e48 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst1/defs". - include "subst0/defs.ma". inductive subst1 (i: nat) (v: T) (t1: T): T \to Prop \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/fwd.ma index 317086097..c7eef274d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst1/fwd". - include "subst1/defs.ma". include "subst0/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/props.ma index a933775b7..f16462a86 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst1/props". - include "subst1/defs.ma". include "subst0/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/subst1.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/subst1.ma index b8e016395..797c1f1db 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/subst1.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/subst1/subst1.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/subst1/subst1". - include "subst1/fwd.ma". include "subst0/subst0.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/defs.ma index 0a1853ded..598876804 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tau0/defs". - include "G/defs.ma". include "getl/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/props.ma index 9baf6cb96..ddba3d947 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau0/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tau0/props". - include "tau0/defs.ma". include "getl/drop.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/cnt.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/cnt.ma index 845ea8933..4419db104 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/cnt.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/cnt.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tau1/cnt". - include "tau1/props.ma". include "cnt/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/defs.ma index 09a531fbc..aeeea9566 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tau1/defs". - include "tau0/defs.ma". inductive tau1 (g: G) (c: C) (t1: T): T \to Prop \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/props.ma index 30ee3158c..434611c57 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tau1/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tau1/props". - include "tau1/defs.ma". include "tau0/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma index daf2a250e..72517f559 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/theory.ma @@ -14,8 +14,6 @@ (* 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". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/defs.ma index ad412abf3..51437021c 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tlist/defs". - include "T/defs.ma". inductive TList: Set \def diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/props.ma index fd6e7db98..518fc312a 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlist/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tlist/props". - include "tlist/defs.ma". theorem tslt_wf__q_ind: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/defs.ma index f5acb3e27..3e24d5adf 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tlt/defs". - include "T/defs.ma". definition wadd: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/props.ma index b75bc8053..56f46e4ea 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/tlt/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/tlt/props". - include "tlt/defs.ma". theorem wadd_le: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity.ma index 0e132c76a..f285aa538 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/arity". - include "ty3/pr3_props.ma". include "arity/pr3.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props.ma index b83158516..2249354ab 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/arity_props". - include "ty3/arity.ma". include "ty3/fwd.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/dec.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/dec.ma index 94280cc8f..4121b6018 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/dec.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/dec.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/dec". - include "ty3/pr3_props.ma". include "pc3/dec.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/defs.ma index 772986fc3..33628e22d 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs". - include "G/defs.ma". include "pc3/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma index d6a141293..8a7506ceb 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/fsubst0". - include "ty3/props.ma". include "pc3/fsubst0.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fwd.ma index 6cbdaf806..60d2b11ee 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/fwd". - include "ty3/defs.ma". include "pc3/props.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma index a23a8ad66..1d5a2f7ef 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/nf2". - include "ty3/arity.ma". include "pc3/nf2.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma index 13b7b98fe..46d1784f6 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3". - include "csubt/ty3.ma". include "ty3/subst1.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma index aa574990d..8e3dfb9e6 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props". - include "ty3/pr3.ma". theorem ty3_cred_pr2: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma index c7c2b05ba..a2c71de45 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/props.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/props". - include "ty3/fwd.ma". include "pc3/fwd.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma index 1f1bd3630..3ae10ea9f 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/subst1". - include "ty3/props.ma". include "pc3/subst1.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma index 67d458408..f7221d81b 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/tau0". - include "ty3/pr3_props.ma". include "tau0/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/defs.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/defs.ma index dff8bb8cc..cd6638c54 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/defs.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/defs.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/wcpr0/defs". - include "pr0/defs.ma". include "C/defs.ma". diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/fwd.ma index 359d38544..0b4723fcb 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/fwd.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/fwd.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/wcpr0/fwd". - include "wcpr0/defs.ma". theorem wcpr0_gen_sort: diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/getl.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/getl.ma index f52805131..41e0cb34a 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/getl.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/wcpr0/getl.ma @@ -14,8 +14,6 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/wcpr0/getl". - include "wcpr0/defs.ma". include "getl/props.ma". -- 2.39.2