X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Fdrop_lreq.ma;h=0165a8255dce02e6aa1b3982c44436580c142dc2;hb=658c000ee2ea2da04cf29efc0acdaf16364fbf5e;hp=0b777278e618b64b8a3734d85e9662535a8201f4;hpb=1994fe8e6355243652770f53a02db5fdf26915f0;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/drop_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/drop_lreq.ma
index 0b777278e..0165a8255 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/drop_lreq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/drop_lreq.ma
@@ -37,7 +37,7 @@ lemma lreq_drop_trans_be: ∀L1,L2,l,m. L1 ⩬[l, m] L2 →
   [ #_ destruct >ypred_succ
     /2 width=3 by drop_pair, ex2_intro/
   | lapply (ylt_inv_O1 i ?) /2 width=1 by ylt_inj/
-    #H <H -H #H lapply (ylt_inv_succ … H) -H
+    #H <H -H #H lapply (ylt_inv_succ … H) -H <yminus_SO2
     #Him elim (IHL12 … HLK1) -IHL12 -HLK1 // -Him
     >yminus_succ <yminus_inj /3 width=3 by drop_drop_lt, ex2_intro/
   ]