- parallel reduction for local environments: we proved the equivalence

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

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 ad0c002b4c4e3fe0fde97b1c4ef6f9176f4b12bf..d9d7042213b8bf7a53cb37a6cba4e15417ffdf6d 100644 (file)
--- 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.