commit completed:

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / llpx.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx.ma
index 17bcd5a7a7a3a4b0fbe17f8289189c7cac3fa321..3276008b4f67dbde746087c18fdc7d3d1a11ee87 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/lazypredsn_7.ma".
-include "basic_2/reduction/llpr.ma".
+include "basic_2/relocation/llpx_sn.ma".
 include "basic_2/reduction/cpx.ma".
 
 (* LAZY SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ***************)
@@ -67,6 +67,3 @@ lemma llpx_lref: ∀h,g,I,G,L1,L2,K1,K2,V1,V2,d,i. d ≤ yinj i →
 
 lemma llpx_refl: ∀h,g,G,T,d. reflexive … (llpx h g G d T).
 /2 width=1 by llpx_sn_refl/ qed.
-
-lemma llpr_llpx: ∀h,g,G,L1,L2,T,d. ⦃G, L1⦄ ⊢ ➡[T, d] L2 → ⦃G, L1⦄ ⊢ ➡[h, g, T, d] L2.
-/3 width=3 by llpx_sn_co, cpr_cpx/ qed.