X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funfold%2Ftpss.ma;h=ba88f64e993e94c98beb5421b11fc4b93ec5d866;hb=8ff4315142253a1a0478b67c07dddf70c36f50cd;hp=93916208b649a6d301c53ab4ef1e56f9d6417871;hpb=e8998d29ab83e7b6aa495a079193705b2f6743d3;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
index 93916208b..ba88f64e9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
@@ -40,12 +40,15 @@ qed-.
 
 (* Basic properties *********************************************************)
 
+lemma tps_tpss: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
+/2 width=1/ qed.
+
 lemma tpss_strap1: ∀L,T1,T,T2,d,e.
-                   L ⊢ T1 ▶* [d, e] T → L ⊢ T ▶ [d, e] T2 → L ⊢ T1 ▶* [d, e] T2. 
+                   L ⊢ T1 ▶* [d, e] T → L ⊢ T ▶ [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
 /2 width=3/ qed.
 
 lemma tpss_strap2: ∀L,T1,T,T2,d,e.
-                   L ⊢ T1 ▶ [d, e] T → L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2. 
+                   L ⊢ T1 ▶ [d, e] T → L ⊢ T ▶* [d, e] T2 → L ⊢ T1 ▶* [d, e] T2.
 /2 width=3/ qed.
 
 lemma tpss_lsubs_trans: ∀L1,T1,T2,d,e. L1 ⊢ T1 ▶* [d, e] T2 →
@@ -134,7 +137,7 @@ lemma tpss_inv_gref1: ∀L,T2,p,d,e. L ⊢ §p ▶* [d, e] T2 → T2 = §p.
 qed-.
 
 lemma tpss_inv_bind1: ∀d,e,L,a,I,V1,T1,U2. L ⊢ ⓑ{a,I} V1. T1 ▶* [d, e] U2 →
-                      ∃∃V2,T2. L ⊢ V1 ▶* [d, e] V2 & 
+                      ∃∃V2,T2. L ⊢ V1 ▶* [d, e] V2 &
                                L. ⓑ{I} V2 ⊢ T1 ▶* [d + 1, e] T2 &
                                U2 = ⓑ{a,I} V2. T2.
 #d #e #L #a #I #V1 #T1 #U2 #H @(tpss_ind … H) -U2
@@ -164,7 +167,7 @@ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
-lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → #{T1} ≤ #{T2}.
+lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → ♯{T1} ≤ ♯{T2}.
 #L #T1 #T2 #d #e #H @(tpss_ind … H) -T2 //
 #T #T2 #_ #HT2 #IHT1
 lapply (tps_fwd_tw … HT2) -HT2 #HT2
@@ -179,4 +182,3 @@ lemma tpss_fwd_shift1: ∀L,L1,T1,T,d,e. L ⊢ L1 @@ T1 ▶*[d, e] T →
   elim (tps_fwd_shift1 … H0) -H0 #L2 #T2 #HL02 #H destruct /2 width=4/
 ]
 qed-.
-  
\ No newline at end of file