X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Funfold%2Ftpss.ma;h=26dd58ee6b04cb30349b86fb79c1ce6719a867de;hb=cc21d0caa6229b7d1a905f9b62de2af4f40cc863;hp=a48f52ade156674fb5fca5a6b5d94f0a49bb1a14;hpb=039f4f6db3a3c128959cd471eb78f575906e07b6;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 a48f52ade..26dd58ee6 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.