X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fi_dynamic%2Fntas_nta_ind.ma;h=41a304476b9269a629965ceed35c6f219ff9bf44;hb=67fe9cec87e129a2a41c75d7ed8456a6f3314421;hp=ec6b81822c4d8ffa968e54285746b88b7261bf57;hpb=86861e6f031df66824a381527dfe847029ff72bc;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta_ind.ma b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta_ind.ma
index ec6b81822..41a304476 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta_ind.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta_ind.ma
@@ -48,12 +48,12 @@ qed-.
 lemma nta_ind_cnv (h) (a) (Q:relation4 …):
       (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
       (∀G,K,V,W,U.
-        ⦃G,K⦄ ⊢ V :[h,a] W → ⬆*[1] W ≘ U →
+        ⦃G,K⦄ ⊢ V :[h,a] W → ⇧*[1] W ≘ U →
         Q G K V W → Q G (K.ⓓV) (#0) U
       ) →
-      (∀G,K,W,U. ⦃G,K⦄ ⊢ W ![h,a] → ⬆*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
+      (∀G,K,W,U. ⦃G,K⦄ ⊢ W ![h,a] → ⇧*[1] W ≘ U → Q G (K.ⓛW) (#0) U) →
       (∀I,G,K,W,U,i.
-        ⦃G,K⦄ ⊢ #i :[h,a] W → ⬆*[1] W ≘ U →
+        ⦃G,K⦄ ⊢ #i :[h,a] W → ⇧*[1] W ≘ U →
         Q G K (#i) W → Q G (K.ⓘ{I}) (#↑i) U
       ) →
       (∀p,I,G,K,V,T,U.