- notation restyling ...

[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 8bf9f197d38c57045a340fb73e06c9216ef82aa1..473f813b6aafb5fa283be7ecce7883ff557d56b2 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
@@ -17,9 +17,9 @@ include "Basic_2/substitution/ltps_ldrop.ma".
 
 (* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
 
-lemma ltps_tps_conf_ge: â\88\80L0,T2,U2,d2,e2. L0 â\8a¢ T2 [d2, e2] â\89« U2 →
-                        â\88\80L1,d1,e1. L0 [d1, e1] â\89« L1 → d1 + e1 ≤ d2 →
-                        L1 â\8a¢ T2 [d2, e2] â\89« U2.
+lemma ltps_tps_conf_ge: â\88\80L0,T2,U2,d2,e2. L0 â\8a¢ T2 [d2, e2] â\96¶ U2 →
+                        â\88\80L1,d1,e1. L0 [d1, e1] â\96¶ L1 → d1 + e1 ≤ d2 →
+                        L1 â\8a¢ T2 [d2, e2] â\96¶ 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: â\88\80L0,T2,U2,d2,e2. L0 â\8a¢ T2 [d2, e2] â\89« U2 →
-                     â\88\80L1,d1,e1. L0 [d1, e1] â\89« L1 →
-                     â\88\83â\88\83T. L1 â\8a¢ T2 [d2, e2] â\89« T &
-                          L1 â\8a¢ U2 [d1, e1] â\89« T.
+lemma ltps_tps_conf: â\88\80L0,T2,U2,d2,e2. L0 â\8a¢ T2 [d2, e2] â\96¶ U2 →
+                     â\88\80L1,d1,e1. L0 [d1, e1] â\96¶ L1 →
+                     â\88\83â\88\83T. L1 â\8a¢ T2 [d2, e2] â\96¶ T &
+                          L1 â\8a¢ U2 [d1, e1] â\96¶ 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: â\88\80L0,T2,U2,d2,e2. L0 â\8a¢ T2 [d2, e2] â\89« U2 →
-                         â\88\80L1,d1,e1. L1 [d1, e1] â\89« L0 → d1 + e1 ≤ d2 →
-                         L1 â\8a¢ T2 [d2, e2] â\89« U2.
+lemma ltps_tps_trans_ge: â\88\80L0,T2,U2,d2,e2. L0 â\8a¢ T2 [d2, e2] â\96¶ U2 →
+                         â\88\80L1,d1,e1. L1 [d1, e1] â\96¶ L0 → d1 + e1 ≤ d2 →
+                         L1 â\8a¢ T2 [d2, e2] â\96¶ 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: â\88\80L0,T2,U2,d2,e2. L0 â\8a¢ T2 [d2, e2] â\89« U2 →
-                      â\88\80L1,d1,e1. L1 [d1, e1] â\89« L0 →
-                      â\88\83â\88\83T. L1 â\8a¢ T2 [d2, e2] â\89« T &
-                           L0 â\8a¢ T [d1, e1] â\89« U2.
+lemma ltps_tps_trans: â\88\80L0,T2,U2,d2,e2. L0 â\8a¢ T2 [d2, e2] â\96¶ U2 →
+                      â\88\80L1,d1,e1. L1 [d1, e1] â\96¶ L0 →
+                      â\88\83â\88\83T. L1 â\8a¢ T2 [d2, e2] â\96¶ T &
+                           L0 â\8a¢ T [d1, e1] â\96¶ 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