diamond property of reduction!

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / cpr.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma
index a5d3ca4d3188f38ef9019301d9dfe924108d4c35..6bcfa173e8ec96dfc351c475a5820c71c14026ed 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma
@@ -107,7 +107,3 @@ qed-.
             pr2_gen_csort pr2_gen_cflat pr2_gen_cbind
             pr2_gen_ctail pr2_ctail
 *)
-(* Basic_1: removed local theorems 4:
-            pr0_delta_eps pr0_cong_delta
-            pr2_free_free pr2_free_delta
-*)