update in ground_2 and basic_2 ...

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma
index 27f0bb6e560829c47b98ba4073e1112c29bb0f72..b883ad18e56a76a11157c1f0976c01d5db7d0c7b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/reduction/llpr_ldrop.ma".
+include "basic_2/reduction/cpr_lift.ma".
 include "basic_2/computation/cprs.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
@@ -29,9 +29,6 @@ lapply (ldrop_fwd_drop2 … HLK) -HLK #HLK
 elim (lift_total V1 0 (i+1)) /4 width=12 by cpr_lift, cprs_strap1/
 qed.
 
-lemma cprs_llpr_conf: ∀G. s_r_confluent1 … (cprs G) (llpr G 0).
-/3 width=5 by llpr_cpr_conf, s_r_conf1_LTC1/ qed-.
-
 (* Advanced inversion lemmas ************************************************)
 
 (* Basic_1: was: pr3_gen_lref *)
@@ -47,7 +44,7 @@ lemma cprs_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡* T2 →
 | * #K #V1 #T1 #HLK #HVT1 #HT1
   lapply (ldrop_fwd_drop2 … HLK) #H0LK
   elim (cpr_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T
- /4 width=6 by cprs_strap1, ex3_3_intro, or_intror/
+  /4 width=6 by cprs_strap1, ex3_3_intro, or_intror/
 ]
 qed-.