X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fpts_dummy_new%2Fconvertibility.ma;h=23a9c686422c60c9806df7c17d8e3fdf7a8217ce;hb=5d9f7ae4bad2b5926f615141c12942b9a8eb23fb;hp=377d3c890488a0ab5907bfa302a3aa763839decf;hpb=46e87acb755894f9234191d675eeb5db4f5b930b;p=helm.git

diff --git a/matita/matita/lib/pts_dummy_new/convertibility.ma b/matita/matita/lib/pts_dummy_new/convertibility.ma
index 377d3c890..23a9c6864 100644
--- a/matita/matita/lib/pts_dummy_new/convertibility.ma
+++ b/matita/matita/lib/pts_dummy_new/convertibility.ma
@@ -9,8 +9,8 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambda/reduction.ma".
-
+include "pts_dummy/reduction.ma".
+(*
 (*
 inductive T : Type[0] ≝
   | Sort: nat → T
@@ -71,3 +71,4 @@ theorem main1: ∀M,N. CO M N →
   |@(ex_intro … M) @(ex_intro … M) % // % //
   ]
 *)
+*)
\ No newline at end of file