- context-sensitive computation: more properties

[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 e0151531334d640a463b5b7071a9d7cbb8be4c85..ed6ee27e303ded0037c1e99c0a8e2c9553aeb9fe 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,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
+*)