X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fcomputation%2Fcprs.ma;h=ed6ee27e303ded0037c1e99c0a8e2c9553aeb9fe;hb=11a20b624a4b5ed18008678cf6cd46dd9a32634d;hp=e0151531334d640a463b5b7071a9d7cbb8be4c85;hpb=9fc816ac51a681fe122712931f8df19d804a4695;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 e01515313..ed6ee27e3 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma
@@ -82,4 +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 2: clear_pr3_trans pr3_cflat *)
+(* Basic_1: removed theorems 5:
+   clear_pr3_trans pr3_cflat
+   pr3_iso_appl_bind pr3_iso_appls_appl_bind pr3_iso_appls_bind
+*)