X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Fllpx_sn_alt1.ma;h=18872b6716edeb7e92bf8b07676e16dd8e0e81ca;hb=3325b784763ae9e6bac4307463071bb38e5641c9;hp=7e071f24dd1d58f9ea9fbf3b7e2fb624e83b56ca;hpb=a0d25627e80a3a2fe68da954b68f6d541c6dbc34;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt1.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt1.ma
index 7e071f24d..18872b671 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt1.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt1.ma
@@ -107,8 +107,8 @@ lemma llpx_sn_alt1_fwd_lref: ∀R,L1,L2,d,i. llpx_sn_alt1 R d (#i) L1 L2 →
 #R #L1 #L2 #d #i #H elim (llpx_sn_alt1_inv_alt … H) -H
 #HL12 #IH elim (lt_or_ge i (|L1|)) /3 width=1 by or3_intro0, conj/
 elim (ylt_split i d) /3 width=1 by or3_intro1/
-#Hdi #HL1 elim (ldrop_O1_lt … HL1)
-#I1 #K1 #V1 #HLK1 elim (ldrop_O1_lt L2 i) //
+#Hdi #HL1 elim (ldrop_O1_lt (Ⓕ) … HL1)
+#I1 #K1 #V1 #HLK1 elim (ldrop_O1_lt (Ⓕ) L2 i) //
 #I2 #K2 #V2 #HLK2 elim (IH … HLK1 HLK2) -IH
 /3 width=9 by nlift_lref_be_SO, or3_intro2, ex5_5_intro/
 qed-.