- degree assignment, static type assignment, iterated static type

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma
index 659689248795b62367f490a59f3f0ece8d53a83a..069f632f4ff77c7b1c90f865036a5d1882fee1ae 100644 (file)
--- 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 *)