- the relocation properties of cpr are closed!

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

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_tps.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_tps.ma
index 3feca620152b0aeb2d99d807e7b769cfd190297e..e07a701bfe10bf2fad70a598a55fbce22a1a4aa3 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_tps.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_tps.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "Basic_2/substitution/tps_lift.ma".
-include "Basic_2/substitution/ltps_drop.ma".
+include "Basic_2/substitution/ltps_ldrop.ma".
 
 (* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
 
@@ -24,7 +24,7 @@ lemma ltps_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
 [ //
 | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01 #Hde1d2
   lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2
-  lapply (ltps_drop_conf_ge … HL01 … HLK0 ?) -HL01 HLK0 /2/
+  lapply (ltps_ldrop_conf_ge … HL01 … HLK0 ?) -HL01 HLK0 /2/
 | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 #Hde1d2
   @tps_bind [ /2/ | @IHTU2 [3: /2/ |1,2: skip | /2/ ] ] (**) (* /3/ is too slow *)
 | /3/
@@ -40,19 +40,19 @@ lemma ltps_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
 [ /2/
 | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01
   elim (lt_or_ge i2 d1) #Hi2d1
-  [ elim (ltps_drop_conf_le … HL01 … HLK0 ?) -HL01 HLK0 /2/ #X #H #HLK1
+  [ elim (ltps_ldrop_conf_le … HL01 … HLK0 ?) -HL01 HLK0 /2/ #X #H #HLK1
     elim (ltps_inv_tps11 … H ?) -H [2: /2/ ] #K1 #V1 #_ #HV01 #H destruct -X;
-    lapply (drop_fwd_drop2 … HLK1) #H
+    lapply (ldrop_fwd_ldrop2 … HLK1) #H
     elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
     lapply (tps_lift_ge … HV01 … H HVW0 HVW1 ?) -H HV01 HVW0 // >arith_a2 /3/
   | elim (lt_or_ge i2 (d1 + e1)) #Hde1i2
-    [ elim (ltps_drop_conf_be … HL01 … HLK0 ? ?) -HL01 HLK0 [2,3: /2/ ] #X #H #HLK1
+    [ elim (ltps_ldrop_conf_be … HL01 … HLK0 ? ?) -HL01 HLK0 [2,3: /2/ ] #X #H #HLK1
       elim (ltps_inv_tps21 … H ?) -H [2: /2/ ] #K1 #V1 #_ #HV01 #H destruct -X;
-      lapply (drop_fwd_drop2 … HLK1) #H
+      lapply (ldrop_fwd_ldrop2 … HLK1) #H
       elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
       lapply (tps_lift_ge … HV01 … H HVW0 HVW1 ?) -H HV01 HVW0 // normalize #HW01
       lapply (tps_weak … HW01 d1 e1 ? ?) [2,3: /3/ ] >arith_i2 //
-    | lapply (ltps_drop_conf_ge … HL01 … HLK0 ?) -HL01 HLK0 /3/
+    | lapply (ltps_ldrop_conf_ge … HL01 … HLK0 ?) -HL01 HLK0 /3/
     ]
   ]
 | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
@@ -71,7 +71,7 @@ lemma ltps_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
 [ //
 | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 #Hde1d2
   lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2
-  lapply (ltps_drop_trans_ge … HL10 … HLK0 ?) -HL10 HLK0 /2/
+  lapply (ltps_ldrop_trans_ge … HL10 … HLK0 ?) -HL10 HLK0 /2/
 | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 #Hde1d2
   @tps_bind [ /2/ | @IHTU2 [3: /2/ |1,2: skip | /2/ ] ] (**) (* /3/ is too slow *)
 | /3/
@@ -87,19 +87,19 @@ lemma ltps_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
 [ /2/
 | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10
   elim (lt_or_ge i2 d1) #Hi2d1
-  [ elim (ltps_drop_trans_le … HL10 … HLK0 ?) -HL10 /2/ #X #H #HLK1
+  [ elim (ltps_ldrop_trans_le … HL10 … HLK0 ?) -HL10 /2/ #X #H #HLK1
     elim (ltps_inv_tps12 … H ?) -H [2: /2/ ] #K1 #V1 #_ #HV01 #H destruct -X;
-    lapply (drop_fwd_drop2 … HLK0) -HLK0 #H
+    lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #H
     elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
     lapply (tps_lift_ge … HV01 … H HVW1 HVW0 ?) -H HV01 HVW0 // >arith_a2 /3/
   | elim (lt_or_ge i2 (d1 + e1)) #Hde1i2
-    [ elim (ltps_drop_trans_be … HL10 … HLK0 ? ?) -HL10 [2,3: /2/ ] #X #H #HLK1
+    [ elim (ltps_ldrop_trans_be … HL10 … HLK0 ? ?) -HL10 [2,3: /2/ ] #X #H #HLK1
       elim (ltps_inv_tps22 … H ?) -H [2: /2/ ] #K1 #V1 #_ #HV01 #H destruct -X;
-      lapply (drop_fwd_drop2 … HLK0) -HLK0 #H
+      lapply (ldrop_fwd_ldrop2 … HLK0) -HLK0 #H
       elim (lift_total V1 0 (i2 + 1)) #W1 #HVW1
       lapply (tps_lift_ge … HV01 … H HVW1 HVW0 ?) -H HV01 HVW0 // normalize #HW01
       lapply (tps_weak … HW01 d1 e1 ? ?) [2,3: /3/ ] >arith_i2 //
-    | lapply (ltps_drop_trans_ge … HL10 … HLK0 ?) -HL10 HLK0 /3/
+    | lapply (ltps_ldrop_trans_ge … HL10 … HLK0 ?) -HL10 HLK0 /3/
     ]
   ]
 | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10