X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Funfold%2Fltpss_ldrop.ma;h=b52cedae7698c826d1f7770b99574a408e9f5a50;hb=70ac3a792389497103fb80b5a1a144706addb7cb;hp=f042449aee72c446e149446a11f955c8b1537913;hpb=0aa60d67f17b528b896e05bbd01038cbc195f69d;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ldrop.ma
index f042449ae..b52cedae7 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ldrop.ma
@@ -17,21 +17,21 @@ include "Basic_2/unfold/ltpss.ma".
 
 (* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
 
-lemma ltpss_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 →
-                           ∀L2,e2. ⇓[0, e2] L0 ≡ L2 →
-                           d1 + e1 ≤ e2 → ⇓[0, e2] L1 ≡ L2.
+lemma ltpss_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 →
+                           ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
+                           d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
 #L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1 // /3 width=6/
 qed.
 
-lemma ltpss_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
-                            ∀L2,e2. ⇓[0, e2] L0 ≡ L2 →
-                            d1 + e1 ≤ e2 → ⇓[0, e2] L1 ≡ L2.
+lemma ltpss_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶* L0 →
+                            ∀L2,e2. ⇩[0, e2] L0 ≡ L2 →
+                            d1 + e1 ≤ e2 → ⇩[0, e2] L1 ≡ L2.
 #L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 // /3 width=6/
 qed.
 
-lemma ltpss_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 →
-                           ∀L2,e2. ⇓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
-                           ∃∃L. L2 [0, d1 + e1 - e2] ≫* L & ⇓[0, e2] L1 ≡ L.
+lemma ltpss_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 →
+                           ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
+                           ∃∃L. L2 [0, d1 + e1 - e2] ▶* L & ⇩[0, e2] L1 ≡ L.
 #L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1
 [ /2 width=3/
 | #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1
@@ -40,9 +40,9 @@ lemma ltpss_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 →
 ]
 qed.
 
-lemma ltpss_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
-                            ∀L2,e2. ⇓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
-                            ∃∃L. L [0, d1 + e1 - e2] ≫* L2 & ⇓[0, e2] L1 ≡ L.
+lemma ltpss_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ▶* L0 →
+                            ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
+                            ∃∃L. L [0, d1 + e1 - e2] ▶* L2 & ⇩[0, e2] L1 ≡ L.
 #L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0
 [ /2 width=3/
 | #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1
@@ -51,9 +51,9 @@ lemma ltpss_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
 ]
 qed.
 
-lemma ltpss_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 →
-                           ∀L2,e2. ⇓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
-                           ∃∃L. L2 [d1 - e2, e1] ≫* L & ⇓[0, e2] L1 ≡ L.
+lemma ltpss_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 →
+                           ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
+                           ∃∃L. L2 [d1 - e2, e1] ▶* L & ⇩[0, e2] L1 ≡ L.
 #L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1
 [ /2 width=3/
 | #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #He2d1
@@ -62,9 +62,9 @@ lemma ltpss_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 →
 ]
 qed.
 
-lemma ltpss_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
-                            ∀L2,e2. ⇓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
-                            ∃∃L. L [d1 - e2, e1] ≫* L2 & ⇓[0, e2] L1 ≡ L.
+lemma ltpss_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ▶* L0 →
+                            ∀L2,e2. ⇩[0, e2] L0 ≡ L2 → e2 ≤ d1 →
+                            ∃∃L. L [d1 - e2, e1] ▶* L2 & ⇩[0, e2] L1 ≡ L.
 #L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0
 [ /2 width=3/
 | #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #He2d1