X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fsubstitution%2Fldrop.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fsubstitution%2Fldrop.ma;h=2b8f3f9535ba442e2fda7f3e7cdfb4a9aa7e606d;hb=9aa9a54946719d3fdb4cadb7c7d33fd13956c083;hp=db31dfaab4d2bc0c827dc39c1631324497904adc;hpb=db63f65c35efaa93d0a2cc00a194549e791975c9;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma
index db31dfaab..2b8f3f953 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma
@@ -152,17 +152,17 @@ lemma ldrop_lsubs_ldrop1_abbr: ∀L1,L2,d,e. L1 [d, e] ≼ L2 →
   [ -IHL12 -Hie destruct
     <minus_n_O <minus_plus_m_m // /2 width=3/
   | -HL12
-    elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >arith_g1 // /3 width=3/
+    elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >minus_minus_comm >arith_b1 // /4 width=3/
   ]
 | #L1 #L2 #I #V1 #V2 #e #_ #IHL12 #K1 #W #i #H #_ #Hie
   elim (ldrop_inv_O1 … H) -H * #Hi #HLK1
   [ -IHL12 -Hie -Hi destruct
-  | elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >arith_g1 // /3 width=3/
+  | elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hie >minus_minus_comm >arith_b1 // /3 width=3/
   ]
 | #L1 #L2 #I1 #I2 #V1 #V2 #d #e #_ #IHL12 #K1 #V #i #H #Hdi >plus_plus_comm_23 #Hide
-  lapply (plus_S_le_to_pos … Hdi) #Hi
+  elim (le_inv_plus_l … Hdi) #Hdim #Hi
   lapply (ldrop_inv_ldrop1 … H ?) -H // #HLK1
-  elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 /2 width=1/ -Hdi -Hide >arith_g1 // /3 width=3/
+  elim (IHL12 … HLK1 ? ?) -IHL12 -HLK1 // /2 width=1/ -Hdi -Hide >minus_minus_comm >arith_b1 // /3 width=3/
 ]
 qed.