commit completed:

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / llpx_ldrop.ma

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 0b9d88b9983c9ea58f1fb5b20217d429ae384d19..3e4bcab8f50a36a62417c6685c22a14552a65616 100644 (file)
--- 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 *******************************************)