X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fsubstitution%2Fltps_tps.ma;h=473f813b6aafb5fa283be7ecce7883ff557d56b2;hb=d833e40ce45e301a01ddd9ea66c29fb2b34bb685;hp=8bf9f197d38c57045a340fb73e06c9216ef82aa1;hpb=9aa9a54946719d3fdb4cadb7c7d33fd13956c083;p=helm.git

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 8bf9f197d..473f813b6 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_tps.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_tps.ma
@@ -17,9 +17,9 @@ include "Basic_2/substitution/ltps_ldrop.ma".
 
 (* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
 
-lemma ltps_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
-                        ∀L1,d1,e1. L0 [d1, e1] ≫ L1 → d1 + e1 ≤ d2 →
-                        L1 ⊢ T2 [d2, e2] ≫ U2.
+lemma ltps_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
+                        ∀L1,d1,e1. L0 [d1, e1] ▶ L1 → d1 + e1 ≤ d2 →
+                        L1 ⊢ T2 [d2, e2] ▶ U2.
 #L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
 [ //
 | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01 #Hde1d2
@@ -32,10 +32,10 @@ lemma ltps_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
 qed.
 
 (* Basic_1: was: subst1_subst1_back *)
-lemma ltps_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
-                     ∀L1,d1,e1. L0 [d1, e1] ≫ L1 →
-                     ∃∃T. L1 ⊢ T2 [d2, e2] ≫ T &
-                          L1 ⊢ U2 [d1, e1] ≫ T.
+lemma ltps_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
+                     ∀L1,d1,e1. L0 [d1, e1] ▶ L1 →
+                     ∃∃T. L1 ⊢ T2 [d2, e2] ▶ T &
+                          L1 ⊢ U2 [d1, e1] ▶ T.
 #L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
 [ /2 width=3/
 | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01
@@ -64,9 +64,9 @@ lemma ltps_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
 ]
 qed.
 
-lemma ltps_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
-                         ∀L1,d1,e1. L1 [d1, e1] ≫ L0 → d1 + e1 ≤ d2 →
-                         L1 ⊢ T2 [d2, e2] ≫ U2.
+lemma ltps_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
+                         ∀L1,d1,e1. L1 [d1, e1] ▶ L0 → d1 + e1 ≤ d2 →
+                         L1 ⊢ T2 [d2, e2] ▶ U2.
 #L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
 [ //
 | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 #Hde1d2
@@ -79,10 +79,10 @@ lemma ltps_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
 qed.
 
 (* Basic_1: was: subst1_subst1 *)
-lemma ltps_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
-                      ∀L1,d1,e1. L1 [d1, e1] ≫ L0 →
-                      ∃∃T. L1 ⊢ T2 [d2, e2] ≫ T &
-                           L0 ⊢ T [d1, e1] ≫ U2.
+lemma ltps_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
+                      ∀L1,d1,e1. L1 [d1, e1] ▶ L0 →
+                      ∃∃T. L1 ⊢ T2 [d2, e2] ▶ T &
+                           L0 ⊢ T [d1, e1] ▶ U2.
 #L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
 [ /2 width=3/
 | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10