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

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 018ca9830..c032c5dd7 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