X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fpts_dummy%2Fpar_reduction.ma;fp=matita%2Fmatita%2Flib%2Fpts_dummy%2Fpar_reduction.ma;h=fec59888c23b963eda89b720868ddb2a348473cb;hb=dbd9f7d4de8286fdd54f4b5609576f33db1050a6;hp=cea1e177b8ed33fc04202bf2b2ba9fe3601cb1f3;hpb=716338697e54d7a7e3602aabdecc2a8a639d683e;p=helm.git

diff --git a/matita/matita/lib/pts_dummy/par_reduction.ma b/matita/matita/lib/pts_dummy/par_reduction.ma
index cea1e177b..fec59888c 100644
--- a/matita/matita/lib/pts_dummy/par_reduction.ma
+++ b/matita/matita/lib/pts_dummy/par_reduction.ma
@@ -9,8 +9,8 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambda/subterms.ma".
-
+include "pts_dummy/subterms.ma".
+(*
 (*
 inductive T : Type[0] ≝
   | Sort: nat → T
@@ -305,3 +305,4 @@ pr Q S ∧ pr P S.
 #P #Q #R #pr1 #pr2 @(ex_intro … (full P)) /3/
 qed.
 
+*)