milestone update in ground_2 and basic_2A

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

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 61002527e2ca56c0050228cf4b5e29b80d599fe9..075ecfa553d3f980667adb099abbcce82e1e9f3f 100644 (file)
--- 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 →