the partial commit continues ...

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / unfold / tpss.ma

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 dd2c219ff94ab8ece693e793359d85d599c08082..a48f52ade156674fb5fca5a6b5d94f0a49bb1a14 100644 (file)
--- 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 *)