X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Fpts_dummy%2Fsubst.ma;h=8583f581027be1e71e38b8c13824736a70f90c4a;hb=0c7cb3c503c0fcab104ad89ebc88683dc9830d06;hp=4f61ef5282fdcf6da367948d7c264526e7ebf87f;hpb=46e87acb755894f9234191d675eeb5db4f5b930b;p=helm.git

diff --git a/matita/matita/lib/pts_dummy/subst.ma b/matita/matita/lib/pts_dummy/subst.ma
index 4f61ef528..8583f5810 100644
--- a/matita/matita/lib/pts_dummy/subst.ma
+++ b/matita/matita/lib/pts_dummy/subst.ma
@@ -9,8 +9,8 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambda/lift.ma".
-
+include "pts_dummy/lift.ma".
+(*
 let rec subst t k a ≝ 
   match t with 
     [ Sort n ⇒ Sort n
@@ -210,3 +210,4 @@ lemma subst_lemma_comm: ∀A,B,C.∀k,i.
   (A [i ≝ B]) [i+k ≝ C] = (A [i+k+1 := C]) [i ≝ B [k ≝ C]].
 #A #B #C #k #i >commutative_plus >subst_lemma //
 qed. 
+*)