X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fmultiple%2Fllpx_sn.ma;h=cf6e4ad769f05997c6f8bafeb0cc4b0f2eeeabfa;hb=658c000ee2ea2da04cf29efc0acdaf16364fbf5e;hp=d954620708cebb9822e37f8e1151432f924bb5db;hpb=1994fe8e6355243652770f53a02db5fdf26915f0;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn.ma
index d95462070..cf6e4ad76 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/llpx_sn.ma
@@ -176,12 +176,12 @@ lemma llpx_sn_ge_up: ∀R,L1,L2,U,lt. llpx_sn R lt U L1 L2 → ∀T,l,m. ⬆[l,
   [ lapply (llpx_sn_fwd_length … HW1) -HW1 #HK12
     lapply (drop_fwd_length … HLK1) lapply (drop_fwd_length … HLK2)
     normalize in ⊢ (%→%→?); -I -W1 -W2 -lt /3 width=1 by llpx_sn_skip, ylt_inj/
-  | /4 width=9 by llpx_sn_lref, yle_inj, le_plus_b/
+  | /3 width=9 by llpx_sn_lref, yle_fwd_plus_sn1/
   ]
 | /2 width=1 by llpx_sn_free/
 | #L1 #L2 #lt #p #HL12 #X #l #m #H #_ >(lift_inv_gref2 … H) -H /2 width=1 by llpx_sn_gref/
 | #a #I #L1 #L2 #W #U #lt #_ #_ #IHV #IHT #X #l #m #H #Hltlm destruct
-  elim (lift_inv_bind2 … H) -H #V #T #HVW >commutative_plus #HTU #H destruct 
+  elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct 
   @(llpx_sn_bind) /2 width=4 by/ (**) (* full auto fails *)
   @(IHT … HTU) /2 width=1 by yle_succ/
 | #I #L1 #L2 #W #U #lt #_ #_ #IHV #IHT #X #l #m #H #Hltlm destruct