X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Fldrops_ldrop.ma;h=302829e62b28d7b5a8620db076fe0e00d17b9d7c;hb=62211b3b2d76ba387663c9e553fbe4d2dbd92c82;hp=958052e5bd1108f57bd38d4df11bef17388a570b;hpb=2ba2dc23443ad764adab652e06d6f5ed10bd912d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma
index 958052e5b..302829e62 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma
@@ -24,12 +24,13 @@ lemma ldrops_ldrop_trans: ∀L1,L,des. ⇩*[Ⓕ, des] L1 ≡ L → ∀L2,i. ⇩[
                                         @⦃i, des⦄ ≡ i0 & des ▭ i ≡ des0.
 #L1 #L #des #H elim H -L1 -L -des
 [ /2 width=7 by ldrops_nil, minuss_nil, at_nil, ex4_3_intro/
-| #L1 #L3 #L #des3 #d #e #_ #HL3 #IHL13 #L2 #i #HL2
+| #L1 #L0 #L #des #d #e #_ #HL0 #IHL0 #L2 #i #HL2
   elim (lt_or_ge i d) #Hid
-  [ elim (ldrop_trans_le … HL3 … HL2) -L /2 width=2 by lt_to_le/
-    #L #HL3 #HL2 elim (IHL13 … HL3) -L3 /3 width=7 by ldrops_cons, minuss_lt, at_lt, ex4_3_intro/
-  | lapply (ldrop_trans_ge … HL3 … HL2 ?) -L // #HL32
-    elim (IHL13 … HL32) -L3 /3 width=7 by minuss_ge, at_ge, ex4_3_intro/
+  [ elim (ldrop_trans_le … HL0 … HL2) -L /2 width=2 by lt_to_le/
+    #L #HL0 #HL2 elim (IHL0 … HL0) -L0 /3 width=7 by ldrops_cons, minuss_lt, at_lt, ex4_3_intro/
+  | lapply (ldrop_trans_ge … HL0 … HL2 ?) -L // #HL02
+    elim (IHL0 … HL02) -L0 /3 width=7 by minuss_ge, at_ge, ex4_3_intro/
   ]
 ]
 qed-.
+