advances on ldrop ....

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

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 7e071f24dd1d58f9ea9fbf3b7e2fb624e83b56ca..18872b6716edeb7e92bf8b07676e16dd8e0e81ca 100644 (file)
--- 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-.