- pts_dummy/pts_dummy_new: non compiling parts commented out

[helm.git] / matita / matita / lib / pts_dummy / subterms.ma

diff --git a/matita/matita/lib/pts_dummy/subterms.ma b/matita/matita/lib/pts_dummy/subterms.ma
index d2b7bee30b76c7fe82e634bd3d15e732f1aff629..3fe2eecd59490e947ec68ff79415ef2c32f1b6e2 100644 (file)
--- 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.
+*)