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

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 faca3d631..472d81e84 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpce.ma
@@ -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