X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fcomputation%2Flprs_cprs.ma;h=bc5beaf2c723fddc04c5d6eecc494efe1f96b036;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hp=a96eaa23a5a2fbaeee1cd4eaf554193caf5a2f28;hpb=d2545ffd201b1aa49887313791386add78fa8603;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/computation/lprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2A/computation/lprs_cprs.ma
index a96eaa23a..bc5beaf2c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/computation/lprs_cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/computation/lprs_cprs.ma
@@ -49,12 +49,12 @@ lemma lprs_ind_alt: ∀G. ∀R:relation lenv.
 (* Properties on context-sensitive parallel computation for terms ***********)
 
 lemma lprs_cpr_trans: ∀G. s_r_transitive … (cpr G) (λ_. lprs G).
-/3 width=5 by s_r_trans_LTC2, lpr_cprs_trans/ qed-.
+/3 width=5 by s_r_trans_CTC2, 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. s_rs_transitive … (cpr G) (λ_. lprs G).
-#G @s_r_to_s_rs_trans @s_r_trans_LTC2
+#G @s_r_to_s_rs_trans @s_r_trans_CTC2
 @s_rs_trans_TC1 /2 width=3 by lpr_cprs_trans/ (**) (* full auto too slow *)
 qed-.