X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fnta_ind.ma;h=29d338f3fcf2962ce71db8f443c3a11f3dde46fb;hp=74f376e7b4adfaa5bc9fcc00386cf2a536889d51;hb=25c634037771dff0138e5e8e3d4378183ff49b86;hpb=bd53c4e895203eb049e75434f638f26b5a161a2b

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
index 74f376e7b..29d338f3f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_ind.ma
@@ -24,12 +24,12 @@ include "basic_2/dynamic/nta_preserve.ma".
 lemma nta_ind_rest_cnv (h) (Q:relation4 …):
       (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
       (∀G,K,V,W,U.
-        ❪G,K❫ ⊢ V :[h,𝟐] W → ⇧*[1] W ≘ U →
+        ❪G,K❫ ⊢ V :[h,𝟐] W → ⇧[1] W ≘ U →
         Q G K V W → Q G (K.ⓓV) (#0) U
       ) →
-      (∀G,K,W,U. ❪G,K❫ ⊢ W ![h,𝟐] → ⇧*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
+      (∀G,K,W,U. ❪G,K❫ ⊢ W ![h,𝟐] → ⇧[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
       (∀I,G,K,W,U,i.
-        ❪G,K❫ ⊢ #i :[h,𝟐] W → ⇧*[1] W ≘ U →
+        ❪G,K❫ ⊢ #i :[h,𝟐] W → ⇧[1] W ≘ U →
         Q G K (#i) W → Q G (K.ⓘ[I]) (#↑i) U
       ) →
       (∀p,I,G,K,V,T,U.
@@ -81,12 +81,12 @@ qed-.
 lemma nta_ind_ext_cnv_mixed (h) (Q:relation4 …):
       (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
       (∀G,K,V,W,U.
-        ❪G,K❫ ⊢ V :[h,𝛚] W → ⇧*[1] W ≘ U →
+        ❪G,K❫ ⊢ V :[h,𝛚] W → ⇧[1] W ≘ U →
         Q G K V W → Q G (K.ⓓV) (#0) U
       ) →
-      (∀G,K,W,U. ❪G,K❫ ⊢ W ![h,𝛚] → ⇧*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
+      (∀G,K,W,U. ❪G,K❫ ⊢ W ![h,𝛚] → ⇧[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
       (∀I,G,K,W,U,i.
-        ❪G,K❫ ⊢ #i :[h,𝛚] W → ⇧*[1] W ≘ U →
+        ❪G,K❫ ⊢ #i :[h,𝛚] W → ⇧[1] W ≘ U →
         Q G K (#i) W → Q G (K.ⓘ[I]) (#↑i) U
       ) →
       (∀p,I,G,K,V,T,U.
@@ -146,12 +146,12 @@ qed-.
 lemma nta_ind_ext_cnv (h) (Q:relation4 …):
       (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
       (∀G,K,V,W,U.
-        ❪G,K❫ ⊢ V :[h,𝛚] W → ⇧*[1] W ≘ U →
+        ❪G,K❫ ⊢ V :[h,𝛚] W → ⇧[1] W ≘ U →
         Q G K V W → Q G (K.ⓓV) (#0) U
       ) →
-      (∀G,K,W,U. ❪G,K❫ ⊢ W ![h,𝛚] → ⇧*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
+      (∀G,K,W,U. ❪G,K❫ ⊢ W ![h,𝛚] → ⇧[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
       (∀I,G,K,W,U,i.
-        ❪G,K❫ ⊢ #i :[h,𝛚] W → ⇧*[1] W ≘ U →
+        ❪G,K❫ ⊢ #i :[h,𝛚] W → ⇧[1] W ≘ U →
         Q G K (#i) W → Q G (K.ⓘ[I]) (#↑i) U
       ) →
       (∀p,I,G,K,V,T,U.