milestone update in ground_2 and basic_2A

[helm.git] / matita / matita / contribs / lambdadelta / basic_2A / computation / lpxs_cpxs.ma

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 c4ba7ccf01832747f7ffdb82a96a2cad55aa986d..5bef4a5ec6546158f1daffd1712654dce4b86027 100644 (file)
--- 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-.