- support for atomic arities and candidates of reducibility started

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / substitution / ltps_ldrop.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma
index 7996f53a6d5d7b75273c05eda967f523a1cf8f80..f777d1cd77c1111797a04a7e4db84915e725d19f 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_ldrop.ma
@@ -23,11 +23,11 @@ lemma ltps_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →
 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
 | //
 | normalize #K0 #K1 #I #V0 #V1 #e1 #_ #_ #IHK01 #L2 #e2 #H #He12
-  lapply (plus_le_weak … He12) #He2
+  elim (le_inv_plus_l … He12) #_ #He2
   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
   lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/
 | #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2
-  lapply (plus_le_weak … Hd1e2) #He2
+  elim (le_inv_plus_l … Hd1e2) #_ #He2
   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
   lapply (IHK01 … HK0L2 ?) -K0 /2 width=1/
 ]
@@ -40,11 +40,11 @@ lemma ltps_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
 | //
 | normalize #K1 #K0 #I #V1 #V0 #e1 #_ #_ #IHK10 #L2 #e2 #H #He12
-  lapply (plus_le_weak … He12) #He2
+  elim (le_inv_plus_l … He12) #_ #He2
   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
   lapply (IHK10 … HK0L2 ?) -K0 /2 width=1/
 | #K0 #K1 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2
-  lapply (plus_le_weak … Hd1e2) #He2
+  elim (le_inv_plus_l … Hd1e2) #_ #He2
   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
   lapply (IHK10 … HK0L2 ?) -IHK10 -HK0L2 /2 width=1/
 ]
@@ -65,7 +65,7 @@ lemma ltps_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →
     elim (IHK01 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
   ]
 | #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 #He2de1
-  lapply (plus_le_weak … Hd1e2) #He2
+  elim (le_inv_plus_l … Hd1e2) #_ #He2
   <minus_le_minus_minus_comm //
   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
   elim (IHK01 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/
@@ -87,7 +87,7 @@ lemma ltps_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
     elim (IHK10 … HK0L2 ? ?) -K0 // /2 width=1/ /3 width=3/
   ]
 | #K1 #K0 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 #He2de1
-  lapply (plus_le_weak … Hd1e2) #He2
+  elim (le_inv_plus_l … Hd1e2) #_ #He2
   <minus_le_minus_minus_comm //
   lapply (ldrop_inv_ldrop1 … H ?) -H // #HK0L2
   elim (IHK10 … HK0L2 ? ?) -K0 /2 width=1/ /3 width=3/