commit completed:

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / llpxs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs.ma
index 154c24f20576646d1766b29db41877f9dd1dde08..750d0b5b1405311bb035224e4fbe9abc83ea9f61 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/llpxs.ma
@@ -14,7 +14,6 @@
 
 include "basic_2/notation/relations/lazypredsnstar_7.ma".
 include "basic_2/reduction/llpx.ma".
-include "basic_2/computation/llprs.ma".
 
 (* LAZY SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS **************)
 
@@ -42,9 +41,6 @@ qed-.
 
 (* Basic properties *********************************************************)
 
-lemma llprs_llpxs: ∀h,g,G,L1,L2,T,d. ⦃G, L1⦄ ⊢ ➡*[T, d] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L2.
-normalize /3 width=3 by llpr_llpx, monotonic_TC/ qed.
-
 lemma llpx_llpxs: ∀h,g,G,L1,L2,T,d. ⦃G, L1⦄ ⊢ ➡[h, g, T, d] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g, T, d] L2.
 normalize /2 width=1 by inj/ qed.