X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Fllpx_sn_ldrop.ma;h=509a836b3afb73bf2118f6fd4db2726c87ea7a09;hb=3325b784763ae9e6bac4307463071bb38e5641c9;hp=04a0f9295007c08e6e2d17ac2037d8a3dd116336;hpb=a0d25627e80a3a2fe68da954b68f6d541c6dbc34;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_ldrop.ma
index 04a0f9295..509a836b3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_ldrop.ma
@@ -134,8 +134,8 @@ lemma llpx_sn_dec: ∀R. (∀I,L,T1,T2. Decidable (R I L T1 T2)) →
   [ #HL12 #d elim (ylt_split i d) /3 width=1 by llpx_sn_skip, or_introl/
     #Hdi elim (lt_or_ge i (|L1|)) #HiL1
     elim (lt_or_ge i (|L2|)) #HiL2 /3 width=1 by or_introl, llpx_sn_free/
-    elim (ldrop_O1_lt … HiL2) #I2 #K2 #V2 #HLK2
-    elim (ldrop_O1_lt … HiL1) #I1 #K1 #V1 #HLK1
+    elim (ldrop_O1_lt (Ⓕ) … HiL2) #I2 #K2 #V2 #HLK2
+    elim (ldrop_O1_lt (Ⓕ) … HiL1) #I1 #K1 #V1 #HLK1
     elim (eq_bind2_dec I2 I1)
     [ #H2 elim (HR I1 K1 V1 V2) -HR
       [ #H3 elim (IH K1 V1 … K2 0) destruct