some renaming and reordering of variables

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / cpx_lleq.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lleq.ma
index 8eb198df41519cc24a4f28924f5460c6399ef5ad..2f608db01214bcc196dcca8bac4d24c0a06bbda8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_lleq.ma
@@ -47,7 +47,7 @@ lemma cpx_lleq_conf: ∀h,o,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, o] T2 →
                      ∀L1. L2 ≡[T1, 0] L1 → ⦃G, L1⦄ ⊢ T1 ➡[h, o] T2.
 /3 width=3 by lleq_cpx_trans, lleq_sym/ qed-.
 
-lemma cpx_lleq_conf_sn: ∀h,o,G. c_r_confluent1 … (cpx h o G) (lleq 0).
+lemma cpx_lleq_conf_sn: ∀h,o,G. b_c_confluent1 … (cpx h o G) (lleq 0).
 /3 width=6 by cpx_llpx_sn_conf, lift_mono, ex2_intro/ qed-.
 
 lemma cpx_lleq_conf_dx: ∀h,o,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, o] T2 →