X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Flsx.ma;h=3c2b01edd1a0f5719d95645ca9b876953f2b02bb;hb=43282d3750af8831c8100c60d75c56fdfb7ff3c9;hp=1abf9c5238f0faa5b2242adde2f4c872cc7d316f;hpb=6c985e4e2e7846a2b9abd0c84569f21c24e9ce2f;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma
index 1abf9c523..3c2b01edd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma
@@ -63,7 +63,7 @@ lemma lsx_gref: ∀h,g,G,L,d,p. G ⊢ ⬊*[h, g, §p, d] L.
 qed.
 
 lemma lsx_ge_up: ∀h,g,G,L,T,U,dt,d,e. dt ≤ yinj d + yinj e →
-                 ⇧[d, e] T ≡ U → G ⊢ ⬊*[h, g, U, dt] L → G ⊢ ⬊*[h, g, U, d] L.
+                 ⬆[d, e] T ≡ U → G ⊢ ⬊*[h, g, U, dt] L → G ⊢ ⬊*[h, g, U, d] L.
 #h #g #G #L #T #U #dt #d #e #Hdtde #HTU #H @(lsx_ind … H) -L
 /5 width=7 by lsx_intro, lleq_ge_up/
 qed-.