X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Flpr.ma;h=afab7f20fb7483115fc59cc2dd17bb8c40211881;hb=65008df95049eb835941ffea1aa682c9253c4c2b;hp=04d5d1a294f09cd6c0f75334945950372e0d6abe;hpb=c07e9b0a3e65c28ca4154fec76a54a9a118fa7e1;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma
index 04d5d1a29..afab7f20f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma
@@ -12,7 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/unfold/lpqs.ma".
+include "basic_2/notation/relations/predsn_2.ma".
+include "basic_2/grammar/lpx_sn.ma".
 include "basic_2/reduction/cpr.ma".
 
 (* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************)
@@ -54,13 +55,6 @@ lemma lpr_append: ∀K1,K2. K1 ⊢ ➡ K2 → ∀L1,L2. L1 ⊢ ➡ L2 →
                   L1 @@ K1 ⊢ ➡ L2 @@ K2.
 /3 width=1 by lpx_sn_append, cpr_append/ qed.
 
-lemma lpqs_lpr: ∀L1,L2. L1 ⊢ ➤* L2 → L1 ⊢ ➡ L2.
-#L1 #L2 #H elim H -L1 -L2 // /3 width=1/
-qed.
-
-lemma lpss_lpr: ∀L1,L2. L1 ⊢ ▶* L2 → L1 ⊢ ➡ L2.
-/3 width=1/ qed.
-
 (* Basic forward lemmas *****************************************************)
 
 lemma lpr_fwd_length: ∀L1,L2. L1 ⊢ ➡ L2 → |L1| = |L2|.