X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_cpce.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_cpce.ma;h=5f1bf31a85728a981da35f341c5a87d7c9913922;hb=f76594123e375bd7852c9421fe260a7bec693a92;hp=472d81e84c892d5a30ef950574f5dcddd30d936e;hpb=a454837a256907d2f83d42ced7be847e10361ea9;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma
index 472d81e84..5f1bf31a8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma
@@ -31,7 +31,7 @@ generalize in match HT1; -HT1
 | #i #H1i #IH #H2i
   elim (drops_ldec_dec L i) [ * #K #W #HLK | -H1i -IH #HnX ]
   [ lapply (cnv_inv_lref_pair … H2i … HLK) -H2i #H2W
-    lapply (csx_inv_lref_pair … HLK H1i) -H1i #H1W
+    lapply (csx_inv_lref_pair_drops … HLK H1i) -H1i #H1W
     elim (cpue_total_csx … H1W) -H1W #X
     elim (abst_dec X) [ * | -IH ]
     [ #p #V1 #U #H destruct * #n #HWU #_