- revision of ground_2 and basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / lsuby.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsuby.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsuby.ma
index 623f8c6aa734680505c86b5059ce0797218a980c..505a0132e62344473aa9d09c4b7622f3d85d44c5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lsuby.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lsuby.ma
@@ -224,7 +224,7 @@ lemma lsuby_drop_trans_be: ∀L1,L2,l,m. L1 ⊆[l, m] L2 →
     /2 width=4 by drop_pair, ex2_2_intro/
   | lapply (ylt_inv_O1 i ?) /2 width=1 by ylt_inj/
     #H <H -H #H lapply (ylt_inv_succ … H) -H
-    #Him elim (IHL12 … HLK1) -IHL12 -HLK1 // -Him
+    #Him elim (IHL12 … HLK1) -IHL12 -HLK1 [2: <yminus_inj ] // -Him
     >yminus_succ <yminus_inj /3 width=4 by drop_drop_lt, ex2_2_intro/
   ]
 | #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #IHL12 #J2 #K2 #W #s #i #HLK2 #Hli