X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fcomputation%2Fcprs.ma;h=a91c9d8b57be18132d8ea2faaaf1d1222dc101e1;hb=bbac36729dab046d61019081c1523af06d876103;hp=ed6ee27e303ded0037c1e99c0a8e2c9553aeb9fe;hpb=2e5d77caec4504b736af370743df2e460e9590f3;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma
index ed6ee27e3..a91c9d8b5 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma
@@ -82,7 +82,7 @@ elim (cpr_inv_cast1 … HU2) -HU2 /3 width=3/ *
 #W2 #T2 #HW2 #HT2 #H destruct /4 width=5/
 qed-.
 
-(* Basic_1: removed theorems 5:
-   clear_pr3_trans pr3_cflat
+(* Basic_1: removed theorems 6:
+   clear_pr3_trans pr3_cflat pr3_gen_bind
    pr3_iso_appl_bind pr3_iso_appls_appl_bind pr3_iso_appls_bind
 *)