X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Flprs_cprs.ma;h=4ade2ddf1b66dbd34aef74b93ccd70bce611a003;hb=e9da8e091898b6e67a2f270581bdc5cdbe80e9b0;hp=ff82ee0a575821cc667e4378c2d58207af84a51d;hpb=3a430d712f9d87185e9271b7b0c5188c5f311e4b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cprs.ma
index ff82ee0a5..4ade2ddf1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cprs.ma
@@ -48,14 +48,14 @@ lemma lprs_ind_alt: ∀G. ∀R:relation lenv.
 
 (* Properties on context-sensitive parallel computation for terms ***********)
 
-lemma lprs_cpr_trans: ∀G. c_r_transitive … (cpr G) (λ_. lprs G).
-/3 width=5 by c_r_trans_LTC2, lpr_cprs_trans/ qed-.
+lemma lprs_cpr_trans: ∀G. b_c_transitive … (cpr G) (λ_. lprs G).
+/3 width=5 by b_c_trans_LTC2, lpr_cprs_trans/ qed-.
 
 (* Basic_1: was just: pr3_pr3_pr3_t *)
 (* Note: alternative proof /3 width=5 by s_r_trans_LTC1, lprs_cpr_trans/ *)
-lemma lprs_cprs_trans: ∀G. c_rs_transitive … (cpr G) (λ_. lprs G).
-#G @c_r_to_c_rs_trans @c_r_trans_LTC2
-@c_rs_trans_TC1 /2 width=3 by lpr_cprs_trans/ (**) (* full auto too slow *)
+lemma lprs_cprs_trans: ∀G. b_rs_transitive … (cpr G) (λ_. lprs G).
+#G @b_c_to_b_rs_trans @b_c_trans_LTC2
+@b_rs_trans_TC1 /2 width=3 by lpr_cprs_trans/ (**) (* full auto too slow *)
 qed-.
 
 lemma lprs_cprs_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 →