X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fpts_dummy%2Ftypes.ma;h=acc0c8b135f0ed386273087989615328662ce807;hb=cd2f5b59215ea771ac137b9a7b115a05175f45d5;hp=0c07d2e70408d3e76c01a88e3a0094447dce62e6;hpb=46e87acb755894f9234191d675eeb5db4f5b930b;p=helm.git

diff --git a/matita/matita/lib/pts_dummy/types.ma b/matita/matita/lib/pts_dummy/types.ma
index 0c07d2e70..acc0c8b13 100644
--- a/matita/matita/lib/pts_dummy/types.ma
+++ b/matita/matita/lib/pts_dummy/types.ma
@@ -9,10 +9,10 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambda/subst.ma".
-include "basics/list.ma".
-
+include "pts_dummy/subst.ma".
+include "basics/lists/list.ma".
 
+(*
 (*************************** substl *****************************)
 
 let rec substl (G:list T) (N:T) : list T ≝  
@@ -190,3 +190,4 @@ lemma tj_subst_0: ∀P,G,v,w. G ⊢_{P} v : w → ∀t,u. w :: G ⊢_{P} t : u 
 #P #G #v #w #Hv #t #u #Ht 
 lapply (substitution_tj … Ht ? ([]) … Hv) normalize //
 qed.
+*)