X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Funfold%2Ftpss.ma;h=93916208b649a6d301c53ab4ef1e56f9d6417871;hb=5613a25cee29ef32a597cb4b44e8f2f4d71c4df0;hp=dd2c219ff94ab8ece693e793359d85d599c08082;hpb=439b6ec33d749ba4e6ae0938e973a85bc23e306e;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma
index dd2c219ff..93916208b 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma
@@ -40,6 +40,10 @@ qed-.
 
 (* Basic properties *********************************************************)
 
+lemma tpss_strap1: ∀L,T1,T,T2,d,e.
+                   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. 
 /2 width=3/ qed.
@@ -104,6 +108,11 @@ lapply (tpss_weak … HT12 0 (d + e) ? ?) -HT12 // #HT12
 lapply (tpss_weak_top … HT12) //
 qed.
 
+lemma tpss_append: ∀K,T1,T2,d,e. K ⊢ T1 ▶* [d, e] T2 →
+                   ∀L. L @@ K ⊢ T1 ▶* [d, e] T2.
+#K #T1 #T2 #d #e #H @(tpss_ind … H) -T2 // /3 width=3/
+qed.
+
 (* Basic inversion lemmas ***************************************************)
 
 (* Note: this can be derived from tpss_inv_atom1 *)
@@ -161,3 +170,13 @@ lemma tpss_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e] T2 → #{T1} ≤ #{T2}.
 lapply (tps_fwd_tw … HT2) -HT2 #HT2
 @(transitive_le … IHT1) //
 qed-.
+
+lemma tpss_fwd_shift1: ∀L,L1,T1,T,d,e. L ⊢ L1 @@ T1 ▶*[d, e] T →
+                       ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
+#L #L1 #T1 #T #d #e #H @(tpss_ind … H) -T
+[ /2 width=4/
+| #T #X #_ #H0 * #L0 #T0 #HL10 #H destruct
+  elim (tps_fwd_shift1 … H0) -H0 #L2 #T2 #HL02 #H destruct /2 width=4/
+]
+qed-.
+  
\ No newline at end of file