X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Fldrops.ma;h=069f632f4ff77c7b1c90f865036a5d1882fee1ae;hb=fdb2c62b58006b82c015ba70b494d50c7860e28f;hp=659689248795b62367f490a59f3f0ece8d53a83a;hpb=4aa431513ffa0ce0accf81e6e9ea4b9314d468e3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma
index 659689248..069f632f4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma
@@ -64,7 +64,7 @@ lemma ldrops_inv_skip2: ∀I,des,i,des2. des ▭ i ≡ des2 →
   >(ldrops_inv_nil … H) -L1 /2 width=7/
 | #des #des2 #d #e #i #Hid #_ #IHdes2 #L1 #K2 #V2 #H
   elim (ldrops_inv_cons … H) -H #L #HL1 #H
-  elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ #K #V >minus_plus #HK2 #HV2 #H destruct
+  elim (ldrop_inv_skip2 … H) -H /2 width=1/ #K #V >minus_plus #HK2 #HV2 #H destruct
   elim (IHdes2 … HL1) -IHdes2 -HL1 #K1 #V1 #des1 #Hdes1 #HK1 #HV1 #X destruct
   @(ex4_3_intro … K1 V1 … ) // [3,4: /2 width=7/ | skip ]
   normalize >plus_minus // @minuss_lt // /2 width=1/ (**) (* explicit constructors, /3 width=1/ is a bit slow *)