X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Flsx.ma;h=5307af43ec859528789047c7abb9824ce7233091;hb=376fd7774ef0fa2f30a4afb25aab6158e3cd04b7;hp=9661a883952c400972ebcc2a273f943db3cb4741;hpb=e4be4188d549da5fde54cdc37a6fb4eb2469c15b;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 9661a8839..5307af43e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma
@@ -62,6 +62,12 @@ lemma lsx_gref: ∀h,g,G,L,d,p. G ⊢ ⋕⬊*[h, g, §p, d] L.
 /3 width=4 by lpxs_fwd_length, lleq_gref/
 qed.
 
+lemma lsx_be: ∀h,g,G,L,T,U,dt,d,e. yinj d ≤ dt → dt ≤ d + e →
+              ⇧[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 #Hddt #Hdtde #HTU #H @(lsx_ind … H) -L
+/5 width=7 by lsx_intro, lleq_be/
+qed-.
+
 (* Basic forward lemmas *****************************************************)
 
 lemma lsx_fwd_bind_sn: ∀h,g,a,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T, d] L →