X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Funfold%2Ftpss.ma;h=a48f52ade156674fb5fca5a6b5d94f0a49bb1a14;hb=039f4f6db3a3c128959cd471eb78f575906e07b6;hp=dd2c219ff94ab8ece693e793359d85d599c08082;hpb=a634c95917dee0fca1d1cf77b6fb7491975128cc;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..a48f52ade 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/tpss.ma
@@ -104,6 +104,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 *)