X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Funfold%2Fltpss_dx.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Funfold%2Fltpss_dx.ma;h=d9d7042213b8bf7a53cb37a6cba4e15417ffdf6d;hb=7bedf1797ba168f0742194b2add69575e5d4a5cd;hp=ad0c002b4c4e3fe0fde97b1c4ef6f9176f4b12bf;hpb=3ca25660341410dd0f8694e6863c7c16f4e912a7;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx.ma
index ad0c002b4..d9d704221 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/ltpss_dx.ma
@@ -233,6 +233,11 @@ lemma ltpss_dx_append_le: ∀K1,K2,d. K1 ▶* [d, |K1| - d] K2 →
                           L1 @@ K1 ▶* [d, |K1| - d + e] L2 @@ K2.
 /2 width=1 by ltpss_dx_append_le_aux/ qed.
 
+lemma ltpss_dx_append_zero: ∀K1,K2. K1 ▶* [0, |K1|] K2 →
+                            ∀L1,L2,e. L1 ▶* [0, e] L2 →
+                            L1 @@ K1 ▶* [0, |K1| + e] L2 @@ K2.
+/2 width=1/ qed.
+
 lemma ltpss_dx_append_ge: ∀K1,K2,d,e. K1 ▶* [d, e] K2 →
                           ∀L1,L2. L1 ▶* [d - |K1|, e] L2 → |K1| ≤ d →
                           L1 @@ K1 ▶* [d, e] L2 @@ K2.