X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funfold%2Ftpss.ma;h=faafb36d16c422160bdb680be2736d2f7d3f872f;hb=514f515ecb8765c68720e880460c2457898d74dc;hp=cc5be0ecab230655c2413f42211b41c8f6201057;hpb=fba384e357ed3c8781fc018c2c16f2b40df144af;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 cc5be0eca..faafb36d1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/tpss.ma
@@ -40,6 +40,9 @@ 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. 
 /2 width=3/ qed.