X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fcomputation%2Flpxs_cpxs.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fcomputation%2Flpxs_cpxs.ma;h=5bef4a5ec6546158f1daffd1712654dce4b86027;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hp=c4ba7ccf01832747f7ffdb82a96a2cad55aa986d;hpb=277fc8ff21ce3dbd6893b1994c55cf5c06a98355;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/computation/lpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2A/computation/lpxs_cpxs.ma
index c4ba7ccf0..5bef4a5ec 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/computation/lpxs_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/computation/lpxs_cpxs.ma
@@ -48,11 +48,11 @@ lemma lpxs_ind_alt: ∀h,g,G. ∀R:relation lenv.
 (* Properties on context-sensitive extended parallel computation for terms **)
 
 lemma lpxs_cpx_trans: ∀h,g,G. s_r_transitive … (cpx h g G) (λ_.lpxs h g G).
-/3 width=5 by s_r_trans_LTC2, lpx_cpxs_trans/ qed-.
+/3 width=5 by s_r_trans_CTC2, lpx_cpxs_trans/ qed-.
 
 (* Note: alternative proof: /3 width=5 by s_r_trans_TC1, lpxs_cpx_trans/ *)
 lemma lpxs_cpxs_trans: ∀h,g,G. s_rs_transitive … (cpx h g G) (λ_.lpxs h g G).
-#h #g #G @s_r_to_s_rs_trans @s_r_trans_LTC2
+#h #g #G @s_r_to_s_rs_trans @s_r_trans_CTC2
 @s_rs_trans_TC1 /2 width=3 by lpx_cpxs_trans/ (**) (* full auto too slow *)
 qed-.