X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Frpx_reqx.ma;h=5cde4c9f69caec246b6517b0576fecc13763bf8a;hp=29964b29c6c9dd78868361f7c0a221af37aaa40c;hb=647504aa72b84eb49be8177b88a9254174e84d4b;hpb=b2cdc4abd9ac87e39bc51b0d9c38daea179adbd5

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma
index 29964b29c..5cde4c9f6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/rpx_reqx.ma
@@ -41,8 +41,8 @@ lemma rpx_bind_dx_split_void (G):
       ∃∃K2. ❪G,K1❫ ⊢ ⬈[ⓑ[p,I]V.T] K2 & K2.ⓧ ≛[T] L2.
 /3 width=5 by rpx_fsge_comp, rex_bind_dx_split_void/ qed-.
 
-lemma rpx_teqx_conf (G): s_r_confluent1 … cdeq (rpx G).
-/2 width=5 by teqx_rex_conf/ qed-.
+lemma rpx_teqx_conf_sn (G): s_r_confluent1 … cdeq (rpx G).
+/2 width=5 by teqx_rex_conf_sn/ qed-.
 
 lemma rpx_teqx_div (G):
       ∀T1,T2. T1 ≛ T2 → ∀L1,L2. ❪G,L1❫ ⊢ ⬈[T2] L2 → ❪G,L1❫ ⊢ ⬈[T1] L2.