X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fnta_cpcs.ma;h=d03ca146b064fa8cd64feaa1f0ff62be81cbee81;hb=67fe9cec87e129a2a41c75d7ed8456a6f3314421;hp=4e505925c9cc92ec08528f72af7bf719dfda80aa;hpb=86861e6f031df66824a381527dfe847029ff72bc;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma
index 4e505925c..d03ca146b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_cpcs.ma
@@ -54,7 +54,7 @@ qed-.
 
 lemma nta_inv_ldec_sn_cnv (h) (a) (G) (K) (V):
       ∀X2. ⦃G,K.ⓛV⦄ ⊢ #0 :[h,a] X2 →
-      ∃∃U. ⦃G,K⦄ ⊢ V ![h,a] & ⬆*[1] V ≘ U & ⦃G,K.ⓛV⦄ ⊢ U ⬌*[h] X2 & ⦃G,K.ⓛV⦄ ⊢ X2 ![h,a].
+      ∃∃U. ⦃G,K⦄ ⊢ V ![h,a] & ⇧*[1] V ≘ U & ⦃G,K.ⓛV⦄ ⊢ U ⬌*[h] X2 & ⦃G,K.ⓛV⦄ ⊢ X2 ![h,a].
 #h #a #G #Y #X #X2 #H
 elim (cnv_inv_cast … H) -H #X1 #HX2 #H1 #HX21 #H2
 elim (cnv_inv_zero … H1) -H1 #Z #K #V #HV #H destruct