X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fpts_dummy%2Fsubterms.ma;h=3fe2eecd59490e947ec68ff79415ef2c32f1b6e2;hb=61a4954847fe3ab75f406573c14645cfd908a79e;hp=d2b7bee30b76c7fe82e634bd3d15e732f1aff629;hpb=46e87acb755894f9234191d675eeb5db4f5b930b;p=helm.git

diff --git a/matita/matita/lib/pts_dummy/subterms.ma b/matita/matita/lib/pts_dummy/subterms.ma
index d2b7bee30..3fe2eecd5 100644
--- a/matita/matita/lib/pts_dummy/subterms.ma
+++ b/matita/matita/lib/pts_dummy/subterms.ma
@@ -9,8 +9,8 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambda/subst.ma".
-
+include "pts_dummy/subst.ma".
+(*
 inductive subterm : T → T → Prop ≝
   | appl : ∀M,N. subterm M (App M N)
   | appr : ∀M,N. subterm N (App M N)
@@ -154,3 +154,4 @@ lemma size_subterm : ∀N,M. subterm N M → size N < size M.
 #N #M #subH (elim subH) normalize //
 #M1 #N1 #P #sub1 #sub2 #size1 #size2 @(transitive_lt … size1 size2)
 qed.
+*)