X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Freduction%2Fllpx_ldrop.ma;h=3e4bcab8f50a36a62417c6685c22a14552a65616;hb=a76f56fdad6348b167376093920650379c9936d4;hp=0b9d88b9983c9ea58f1fb5b20217d429ae384d19;hpb=956df16197063a88b3858e3d212d7ed0f2c5ff46;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_ldrop.ma
index 0b9d88b99..3e4bcab8f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/llpx_ldrop.ma
@@ -55,7 +55,7 @@ lemma llpx_fwd_bind_O_dx: ∀h,g,a,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ➡[h, g, ⓑ{
 (* Advanced properties ******************************************************)
 
 lemma llpx_cpx_conf: ∀h,g,G. s_r_confluent1 … (cpx h g G) (llpx h g G 0).
-/3 width=10 by llpx_sn_cpx_conf, cpx_inv_lift1, cpx_lift/ qed-.
+/3 width=10 by cpx_llpx_sn_conf, cpx_inv_lift1, cpx_lift/ qed-.
 
 (* Inversion lemmas on relocation *******************************************)