X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fcomputation%2Fcpxs_cpxs.ma;h=075ecfa553d3f980667adb099abbcce82e1e9f3f;hp=61002527e2ca56c0050228cf4b5e29b80d599fe9;hb=1fd63df4c77f5c24024769432ea8492748b4ac79;hpb=277fc8ff21ce3dbd6893b1994c55cf5c06a98355

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/computation/cpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2A/computation/cpxs_cpxs.ma
index 61002527e..075ecfa55 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/computation/cpxs_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/computation/cpxs_cpxs.ma
@@ -116,7 +116,7 @@ lemma cpx_bind2: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 →
 (* Advanced properties ******************************************************)
 
 lemma lpx_cpxs_trans: ∀h,g,G. s_rs_transitive … (cpx h g G) (λ_.lpx h g G).
-#h #g #G @s_r_trans_LTC1 /2 width=3 by lpx_cpx_trans/ (**) (* full auto fails *)
+#h #g #G @s_r_trans_CTC1 /2 width=3 by lpx_cpx_trans/ (**) (* full auto fails *)
 qed-.
 
 lemma cpxs_bind2_dx: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 →