still more additions and corrections for the article

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / cnv_cpce.ma

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 faca3d631551475656388ecd95f57a0f09cf9d01..5f1bf31a85728a981da35f341c5a87d7c9913922 100644 (file)
--- 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 #_
@@ -57,7 +57,7 @@ generalize in match HT1; -HT1
 | #p #I #V1 #T1 #_ #IH #H
   elim (cnv_inv_bind … H) -H #HV1 #HT1
   elim (IH … HV1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_pair_sn/ ] #V2 #HV12
-  elim (IH … HT1) [| /3 width=1 by fpb_fpbg, fpb_fqu, fqu_bind_dx/ ] #T2 #HT12
+  elim (IH … HT1) [| /4 width=1 by fpb_fpbg, fpb_fqu, fqu_bind_dx/ ] #T2 #HT12
   /3 width=2 by cpce_bind, ex_intro/
 | #I #V1 #T1 #_ #IH #H
   elim (cnv_fwd_flat … H) -H #HV1 #HT1