X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda-delta%2FBasic-2%2Funfold%2Ftpss_tpss.ma;h=a8492845333c75d7db27c49e501e832f53d1ee8b;hb=95fe49b9bd546ee4f0d27dce7267d7285eb81b01;hp=5cc6b38b7cdc1e9364181c4be356b2c8c358e79e;hpb=85d772f5c3d5c86bbb474ba7ab4a259dc06687f9;p=helm.git

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss_tpss.ma b/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss_tpss.ma
index 5cc6b38b7..a84928453 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss_tpss.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss_tpss.ma
@@ -19,6 +19,12 @@ include "Basic-2/unfold/tpss_lift.ma".
 
 (* Advanced properties ******************************************************)
 
+lemma tpss_tps: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫* T2 → L ⊢ T1 [d, 1] ≫ T2.
+#L #T1 #T2 #d #H @(tpss_ind … H) -H T2 //
+#T #T2 #_ #HT2 #IHT1
+lapply (tps_trans_ge … IHT1 … HT2 ?) //
+qed.
+
 lemma tpss_strip_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 [d1, e1] ≫* T1 →
                      ∀T2,d2,e2. L ⊢ T0 [d2, e2] ≫ T2 →
                      ∃∃T. L ⊢ T1 [d2, e2] ≫ T & L ⊢ T2 [d1, e1] ≫* T.