the partial commit continues ...

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / unfold / ltpss_ldrop.ma

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 4d223834e3f27030fe704461249f70e15a8b7001..8787d594ef82931cb82d5c0749504be29c13d0f6 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_ldrop.ma
@@ -16,7 +16,7 @@ include "basic_2/unfold/ltpss.ma".
 
 (* PARALLEL UNFOLD ON LOCAL ENVIRONMENTS ************************************)
 
-lemma ltpss_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 →
+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 elim H -L0 -L1 -d1 -e1
@@ -33,7 +33,7 @@ lemma ltpss_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 →
 ]
 qed.
 
-lemma ltpss_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶* L0 →
+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 elim H -L1 -L0 -d1 -e1
@@ -50,9 +50,9 @@ lemma ltpss_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶* L0 →
 ]
 qed.
 
-lemma ltpss_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ▶* L1 →
+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.
+                           ∃∃L. L2 ▶* [0, d1 + e1 - e2] L & ⇩[0, e2] L1 ≡ L.
 #L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
 | normalize #L #I #V #L2 #e2 #HL2 #_ #He2
@@ -72,9 +72,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 →
+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.
+                            ∃∃L. L ▶* [0, d1 + e1 - e2] L2 & ⇩[0, e2] L1 ≡ L.
 #L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
 | normalize #L #I #V #L2 #e2 #HL2 #_ #He2
@@ -94,9 +94,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 →
+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.
+                           ∃∃L. L2 ▶* [d1 - e2, e1] L & ⇩[0, e2] L1 ≡ L.
 #L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
 | /2 width=3/
@@ -112,9 +112,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 →
+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.
+                            ∃∃L. L ▶* [d1 - e2, e1] L2 & ⇩[0, e2] L1 ≡ L.
 #L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
 [ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
 | /2 width=3/