- property S4 of strongly normalizing term proved!

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / computation / cprs.ma

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 ed6ee27e303ded0037c1e99c0a8e2c9553aeb9fe..a91c9d8b57be18132d8ea2faaaf1d1222dc101e1 100644 (file)
--- 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
 *)