- pts_dummy/pts_dummy_new: non compiling parts commented out

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

diff --git a/matita/matita/lib/pts_dummy/subst.ma b/matita/matita/lib/pts_dummy/subst.ma
index 4f61ef5282fdcf6da367948d7c264526e7ebf87f..8583f581027be1e71e38b8c13824736a70f90c4a 100644 (file)
--- 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. 
+*)