notation and dependences bug fix

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / unfold / tpss_lift.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma
index f2c39379f023938b3e168ab88cc60b0d9af59dc0..23d571549513f5359e050d3930bda099d3131e58 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma
@@ -21,8 +21,8 @@ include "Basic_2/unfold/tpss.ma".
 
 lemma tpss_subst: ∀L,K,V,U1,i,d,e.
                   d ≤ i → i < d + e →
-                  â\86\93[0, i] L â\89¡ K. ð\9d\95\93{Abbr} V â\86\92 K â\8a¢ V [0, d + e - i - 1] â\89«* U1 â\86\92
-                  â\88\80U2. â\86\91[0, i + 1] U1 â\89¡ U2 â\86\92 L â\8a¢ #i [d, e] â\89«* U2.
+                  â\87\93[0, i] L â\89¡ K. ð\9d\95\93{Abbr} V â\86\92 K â\8a¢ V [0, d + e - i - 1] â\89«* U1 â\86\92
+                  â\88\80U2. â\87\91[0, i + 1] U1 â\89¡ U2 â\86\92 L â\8a¢ #i [d, e] â\89«* U2.
 #L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(tpss_ind … H) -U1
 [ /3 width=4/
 | #U #U1 #_ #HU1 #IHU #U2 #HU12
@@ -39,9 +39,9 @@ qed.
 lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ 𝕒{I} [d, e] ≫* T2 →
                       T2 = 𝕒{I} ∨
                       ∃∃K,V1,V2,i. d ≤ i & i < d + e &
-                                   â\86\93[O, i] L â\89¡ K. ð\9d\95\93{Abbr} V1 &
+                                   â\87\93[O, i] L â\89¡ K. ð\9d\95\93{Abbr} V1 &
                                    K ⊢ V1 [0, d + e - i - 1] ≫* V2 &
-                                   â\86\91[O, i + 1] V2 â\89¡ T2 &
+                                   â\87\91[O, i + 1] V2 â\89¡ T2 &
                                    I = LRef i.
 #L #T2 #I #d #e #H @(tpss_ind … H) -T2
 [ /2 width=1/
@@ -59,16 +59,16 @@ qed-.
 lemma tpss_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ≫* T2 →
                       T2 = #i ∨
                       ∃∃K,V1,V2. d ≤ i & i < d + e &
-                                 â\86\93[O, i] L â\89¡ K. ð\9d\95\93{Abbr} V1 &
+                                 â\87\93[O, i] L â\89¡ K. ð\9d\95\93{Abbr} V1 &
                                  K ⊢ V1 [0, d + e - i - 1] ≫* V2 &
-                                 â\86\91[O, i + 1] V2 â\89¡ T2.
+                                 â\87\91[O, i + 1] V2 â\89¡ T2.
 #L #T2 #i #d #e #H
 elim (tpss_inv_atom1 … H) -H /2 width=1/
 * #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct /3 width=6/
 qed-.
 
 lemma tpss_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫* T2 →
-                         â\88\80K,V. â\86\93[0, d] L â\89¡ K. ð\9d\95\93{Abst} V â\86\92 T1 = T2.
+                         â\88\80K,V. â\87\93[0, d] L â\89¡ K. ð\9d\95\93{Abst} V â\86\92 T1 = T2.
 #L #T1 #T2 #d #H #K #V #HLK @(tpss_ind … H) -T2 //
 #T #T2 #_ #HT2 #IHT <(tps_inv_refl_SO2 … HT2 … HLK) //
 qed-.
@@ -76,8 +76,8 @@ qed-.
 (* Relocation properties ****************************************************)
 
 lemma tpss_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 →
-                    â\88\80L,U1,d,e. dt + et â\89¤ d â\86\92 â\86\93[d, e] L â\89¡ K â\86\92
-                    â\86\91[d, e] T1 â\89¡ U1 â\86\92 â\88\80U2. â\86\91[d, e] T2 â\89¡ U2 â\86\92
+                    â\88\80L,U1,d,e. dt + et â\89¤ d â\86\92 â\87\93[d, e] L â\89¡ K â\86\92
+                    â\87\91[d, e] T1 â\89¡ U1 â\86\92 â\88\80U2. â\87\91[d, e] T2 â\89¡ U2 â\86\92
                     L ⊢ U1 [dt, et] ≫* U2.
 #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdetd #HLK #HTU1 @(tpss_ind … H) -T2
 [ #U2 #H >(lift_mono … HTU1 … H) -H //
@@ -90,8 +90,8 @@ qed.
 
 lemma tpss_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 →
                     ∀L,U1,d,e. dt ≤ d → d ≤ dt + et →
-                    â\86\93[d, e] L â\89¡ K â\86\92 â\86\91[d, e] T1 â\89¡ U1 â\86\92
-                    â\88\80U2. â\86\91[d, e] T2 â\89¡ U2 â\86\92 L â\8a¢ U1 [dt, et + e] â\89«* U2.
+                    â\87\93[d, e] L â\89¡ K â\86\92 â\87\91[d, e] T1 â\89¡ U1 â\86\92
+                    â\88\80U2. â\87\91[d, e] T2 â\89¡ U2 â\86\92 L â\8a¢ U1 [dt, et + e] â\89«* U2.
 #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1 @(tpss_ind … H) -T2
 [ #U2 #H >(lift_mono … HTU1 … H) -H //
 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
@@ -102,8 +102,8 @@ lemma tpss_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 →
 qed.
 
 lemma tpss_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 →
-                    â\88\80L,U1,d,e. d â\89¤ dt â\86\92 â\86\93[d, e] L â\89¡ K â\86\92
-                    â\86\91[d, e] T1 â\89¡ U1 â\86\92 â\88\80U2. â\86\91[d, e] T2 â\89¡ U2 â\86\92
+                    â\88\80L,U1,d,e. d â\89¤ dt â\86\92 â\87\93[d, e] L â\89¡ K â\86\92
+                    â\87\91[d, e] T1 â\89¡ U1 â\86\92 â\88\80U2. â\87\91[d, e] T2 â\89¡ U2 â\86\92
                     L ⊢ U1 [dt + e, et] ≫* U2.
 #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hddt #HLK #HTU1 @(tpss_ind … H) -T2
 [ #U2 #H >(lift_mono … HTU1 … H) -H //
@@ -115,9 +115,9 @@ lemma tpss_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 →
 qed.
 
 lemma tpss_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
-                         â\88\80K,d,e. â\86\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\86\91[d, e] T1 â\89¡ U1 â\86\92
+                         â\88\80K,d,e. â\87\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\87\91[d, e] T1 â\89¡ U1 â\86\92
                          dt + et ≤ d →
-                         â\88\83â\88\83T2. K â\8a¢ T1 [dt, et] â\89«* T2 & â\86\91[d, e] T2 â\89¡ U2.
+                         â\88\83â\88\83T2. K â\8a¢ T1 [dt, et] â\89«* T2 & â\87\91[d, e] T2 â\89¡ U2.
 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdetd @(tpss_ind … H) -U2
 [ /2 width=3/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
@@ -126,9 +126,9 @@ lemma tpss_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
 qed.
 
 lemma tpss_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
-                         â\88\80K,d,e. â\86\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\86\91[d, e] T1 â\89¡ U1 â\86\92
+                         â\88\80K,d,e. â\87\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\87\91[d, e] T1 â\89¡ U1 â\86\92
                          dt ≤ d → d + e ≤ dt + et →
-                         â\88\83â\88\83T2. K â\8a¢ T1 [dt, et - e] â\89«* T2 & â\86\91[d, e] T2 â\89¡ U2.
+                         â\88\83â\88\83T2. K â\8a¢ T1 [dt, et - e] â\89«* T2 & â\87\91[d, e] T2 â\89¡ U2.
 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(tpss_ind … H) -U2
 [ /2 width=3/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
@@ -137,9 +137,9 @@ lemma tpss_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
 qed.
 
 lemma tpss_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
-                         â\88\80K,d,e. â\86\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\86\91[d, e] T1 â\89¡ U1 â\86\92
+                         â\88\80K,d,e. â\87\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\87\91[d, e] T1 â\89¡ U1 â\86\92
                          d + e ≤ dt →
-                         â\88\83â\88\83T2. K â\8a¢ T1 [dt - e, et] â\89«* T2 & â\86\91[d, e] T2 â\89¡ U2.
+                         â\88\83â\88\83T2. K â\8a¢ T1 [dt - e, et] â\89«* T2 & â\87\91[d, e] T2 â\89¡ U2.
 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdedt @(tpss_ind … H) -U2
 [ /2 width=3/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
@@ -148,16 +148,16 @@ lemma tpss_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
 qed.
 
 lemma tpss_inv_lift1_eq: ∀L,U1,U2,d,e.
-                         L â\8a¢ U1 [d, e] â\89«* U2 â\86\92 â\88\80T1. â\86\91[d, e] T1 â\89¡ U1 â\86\92 U1 = U2.
+                         L â\8a¢ U1 [d, e] â\89«* U2 â\86\92 â\88\80T1. â\87\91[d, e] T1 â\89¡ U1 â\86\92 U1 = U2.
 #L #U1 #U2 #d #e #H #T1 #HTU1 @(tpss_ind … H) -U2 //
 #U #U2 #_ #HU2 #IHU destruct
 <(tps_inv_lift1_eq … HU2 … HTU1) -HU2 -HTU1 //
 qed.
 
 lemma tpss_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
-                            â\88\80K,d,e. â\86\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\86\91[d, e] T1 â\89¡ U1 â\86\92
+                            â\88\80K,d,e. â\87\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\87\91[d, e] T1 â\89¡ U1 â\86\92
                             dt ≤ d → dt + et ≤ d + e →
-                            â\88\83â\88\83T2. K â\8a¢ T1 [dt, d - dt] â\89«* T2 & â\86\91[d, e] T2 â\89¡ U2.
+                            â\88\83â\88\83T2. K â\8a¢ T1 [dt, d - dt] â\89«* T2 & â\87\91[d, e] T2 â\89¡ U2.
 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(tpss_ind … H) -U2
 [ /2 width=3/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU