From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 7 Dec 2012 16:36:51 +0000 (+0000)
Subject: - pts_dummy/pts_dummy_new: non compiling parts commented out
X-Git-Tag: make_still_working~1406
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dbd9f7d4de8286fdd54f4b5609576f33db1050a6;p=helm.git

- pts_dummy/pts_dummy_new: non compiling parts commented out
- tutorial: some comments added
---

diff --git a/matita/matita/lib/pts_dummy/CC2FO_K.ma b/matita/matita/lib/pts_dummy/CC2FO_K.ma
index 752ed00c0..0983db3ba 100644
--- a/matita/matita/lib/pts_dummy/CC2FO_K.ma
+++ b/matita/matita/lib/pts_dummy/CC2FO_K.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "degree.ma".
-
+include "pts_dummy/degree.ma".
+(*
 (* TO BE PUT ELSEWERE *)
 lemma cons_append_assoc: ∀A,a. ∀l1,l2:list A. (a::l1) @ l2 = a :: (l1 @ l2).
 // qed.
@@ -149,3 +149,4 @@ let rec KI G ≝ match G with
 ].
 
 interpretation "CC2FO: K interpretation (context)" 'IK G = (KI G).
+*)
diff --git a/matita/matita/lib/pts_dummy/CC2FO_K_cube.ma b/matita/matita/lib/pts_dummy/CC2FO_K_cube.ma
index 814ce59fe..b70f731f1 100644
--- a/matita/matita/lib/pts_dummy/CC2FO_K_cube.ma
+++ b/matita/matita/lib/pts_dummy/CC2FO_K_cube.ma
@@ -12,13 +12,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "CC2FO_K.ma".
-include "cube.ma".
-include "inversion.ma".
-
+include "pts_dummy/CC2FO_K.ma".
+include "pts_dummy/cube.ma".
+include "pts_dummy/inversion.ma".
+(*
 (* The K interpretation in the λ-Cube *****************************************)
 
 lemma ki_type: ∀G,t,u. G ⊢_{CC} t : u → u = Sort 1 → 𝕂{G} ⊢_{FO} 𝕂{t}_[G] : u.
 #G #t #u #H elim H -H G t u
 [ #i #j * #_ @ax //
-| #G #A #i #HA #IHA #Heq  
\ No newline at end of file
+| #G #A #i #HA #IHA #Heq  
+*)
diff --git a/matita/matita/lib/pts_dummy/arity.ma b/matita/matita/lib/pts_dummy/arity.ma
index 3df7811c0..b5dd81df7 100644
--- a/matita/matita/lib/pts_dummy/arity.ma
+++ b/matita/matita/lib/pts_dummy/arity.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/ext.ma".
-
+include "pts_dummy/ext.ma".
+(*
 (* ARITIES ********************************************************************)
 
 (* An arity is a normal term representing the functional structure of a term.
@@ -218,3 +218,4 @@ lemma nth_sort_comp: ∀E1,E2. E1 ≅ E2 →
                      ∀i. nth i ? E1 sort ≅ nth i ? E2 sort.
 #E1 #E2 #H #i @(all2_nth … aeq) //
 qed.
+*)
diff --git a/matita/matita/lib/pts_dummy/arity_eval.ma b/matita/matita/lib/pts_dummy/arity_eval.ma
index 6fcf0e0c0..8adcc4873 100644
--- a/matita/matita/lib/pts_dummy/arity_eval.ma
+++ b/matita/matita/lib/pts_dummy/arity_eval.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/arity.ma".
-
+include "pts_dummy/arity.ma".
+(*
 (* ARITY ASSIGNMENT ***********************************************************)
 
 (* the arity type *************************************************************)
@@ -226,3 +226,4 @@ axiom cons_comp: ∀a1,a2. a1 ≅ a2 → ∀E1,E2. E1 ≅ E2 → a1 :: E1 ≅ a2
 axiom pippo: ∀A:Type[0]. ∀a,b,c. (a::b) @ c = a :: b @ c.
 @A qed.
 *)
+*)
diff --git a/matita/matita/lib/pts_dummy/convertibility.ma b/matita/matita/lib/pts_dummy/convertibility.ma
index 045463aaa..3f548c42d 100644
--- a/matita/matita/lib/pts_dummy/convertibility.ma
+++ b/matita/matita/lib/pts_dummy/convertibility.ma
@@ -9,8 +9,8 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambda/reduction.ma".
-
+include "pts_dummy/reduction.ma".
+(*
 (*
 inductive T : Type[0] ≝
   | Sort: nat → T
@@ -71,3 +71,4 @@ theorem main1: ∀M,N. conv M N →
   |@(ex_intro … M) @(ex_intro … M) % // % //
   ]
 *)
+*)
diff --git a/matita/matita/lib/pts_dummy/cube.ma b/matita/matita/lib/pts_dummy/cube.ma
index 8ac3d978c..c143261ad 100644
--- a/matita/matita/lib/pts_dummy/cube.ma
+++ b/matita/matita/lib/pts_dummy/cube.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "convertibility.ma".
-include "types.ma".
-
+include "pts_dummy/convertibility.ma".
+include "pts_dummy/types.ma".
+(*
 (* PURE TYPE SYSTEMS OF THE λ-CUBE ********************************************)
 
 inductive Cube_Ax: nat → nat → Prop ≝
@@ -41,3 +41,4 @@ inductive FO_Re: nat → nat → nat → Prop ≝
 .
 
 definition FO: pts ≝ mk_pts Cube_Ax FO_Re conv.
+*)
diff --git a/matita/matita/lib/pts_dummy/degree.ma b/matita/matita/lib/pts_dummy/degree.ma
index 1fa4ee7ec..61caa58b1 100644
--- a/matita/matita/lib/pts_dummy/degree.ma
+++ b/matita/matita/lib/pts_dummy/degree.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/ext_lambda.ma".
-
+include "pts_dummy/ext_lambda.ma".
+(*
 (* DEGREE ASSIGNMENT **********************************************************)
 
 (* The degree of a term *******************************************************)
@@ -158,3 +158,4 @@ lemma Deg_lift_subst: ∀v,w,G. [║v║_[║G║]] = ║[w]║*_[║G║] →
 >append_Deg >append_Deg <Hvw -Hvw >DegHd_Lift; [2: //]
 >deg_lift; [2,3: >HGk /2/] <(deg_subst … k) // >HGk /2/
 qed.
+*)
diff --git a/matita/matita/lib/pts_dummy/ext.ma b/matita/matita/lib/pts_dummy/ext.ma
index d07234a71..f698ed591 100644
--- a/matita/matita/lib/pts_dummy/ext.ma
+++ b/matita/matita/lib/pts_dummy/ext.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basics/list.ma".
+include "basics/lists/list.ma".
 
 (* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
 
diff --git a/matita/matita/lib/pts_dummy/ext_lambda.ma b/matita/matita/lib/pts_dummy/ext_lambda.ma
index e0455c204..3d4c0c86e 100644
--- a/matita/matita/lib/pts_dummy/ext_lambda.ma
+++ b/matita/matita/lib/pts_dummy/ext_lambda.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/ext.ma".
-include "lambda/subst.ma".
-
+include "pts_dummy/ext.ma".
+include "pts_dummy/subst.ma".
+(*
 (* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
 
 (* substitution ***************************************************************)
@@ -79,3 +79,4 @@ qed.
 
 lemma tsubst_sort: ∀n,l. (Sort n)[/l] = Sort n.
 // qed.
+*)
diff --git a/matita/matita/lib/pts_dummy/inversion.ma b/matita/matita/lib/pts_dummy/inversion.ma
index 0c2c2a98b..63831f078 100644
--- a/matita/matita/lib/pts_dummy/inversion.ma
+++ b/matita/matita/lib/pts_dummy/inversion.ma
@@ -9,8 +9,8 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambda/types.ma".
-
+include "pts_dummy/types.ma".
+(*
 (*
 inductive TJ (p: pts): list T → T → T → Prop ≝
   | ax : ∀i,j. Ax p i j → TJ p (nil T) (Sort i) (Sort j)
@@ -98,3 +98,4 @@ theorem abs_inv: ∀P,G,M,N. G ⊢ _{P} M : N → ∀A,b.M = Lambda A b →
   ]
 qed.
    
+*)
diff --git a/matita/matita/lib/pts_dummy/lift.ma b/matita/matita/lib/pts_dummy/lift.ma
index 27d3d192e..036f8effa 100644
--- a/matita/matita/lib/pts_dummy/lift.ma
+++ b/matita/matita/lib/pts_dummy/lift.ma
@@ -9,7 +9,10 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambda/terms.ma".
+include "pts_dummy/terms.ma".
+
+(* to be put elsewhere *)
+definition if_then_else ≝ λT:Type[0].λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
 
 (* arguments: k is the depth (starts from 0), p is the height (starts from 0) *)
 let rec lift t k p ≝
@@ -32,7 +35,7 @@ notation "↑ _ k ^ n ( M )" non associative with precedence 40 for @{'Lift $n $
 interpretation "Lift" 'Lift n k M = (lift M k n). 
 
 (*** properties of lift ***)
-
+(* BEGIN HERE 
 lemma lift_0: ∀t:T.∀k. lift t k 0 = t.
 #t (elim t) normalize // #n #k cases (leb (S n) k) normalize // 
 qed.
@@ -132,3 +135,4 @@ qed.
 lemma Lift_length: ∀p,G. |Lift G p| = |G|.
 #p #G elim G -G; normalize //
 qed. 
+*)
\ No newline at end of file
diff --git a/matita/matita/lib/pts_dummy/par_reduction.ma b/matita/matita/lib/pts_dummy/par_reduction.ma
index cea1e177b..fec59888c 100644
--- a/matita/matita/lib/pts_dummy/par_reduction.ma
+++ b/matita/matita/lib/pts_dummy/par_reduction.ma
@@ -9,8 +9,8 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambda/subterms.ma".
-
+include "pts_dummy/subterms.ma".
+(*
 (*
 inductive T : Type[0] ≝
   | Sort: nat → T
@@ -305,3 +305,4 @@ pr Q S ∧ pr P S.
 #P #Q #R #pr1 #pr2 @(ex_intro … (full P)) /3/
 qed.
 
+*)
diff --git a/matita/matita/lib/pts_dummy/rc_eval.ma b/matita/matita/lib/pts_dummy/rc_eval.ma
index 3fdeed410..87cfd11dc 100644
--- a/matita/matita/lib/pts_dummy/rc_eval.ma
+++ b/matita/matita/lib/pts_dummy/rc_eval.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/rc_hsat.ma".
-
+include "pts_dummy/rc_hsat.ma".
+(*
 (* THE EVALUATION *************************************************************)
 
 (* The arity of a term t in an environment E *)
@@ -161,3 +161,4 @@ theorem append_cons: ∀(A:Type[0]). ∀(l1,l2:list A). ∀a.
                      (a :: l1) @ l2 = a :: (l1 @ l2).
 // qed.
 *)
+
diff --git a/matita/matita/lib/pts_dummy/rc_hsat.ma b/matita/matita/lib/pts_dummy/rc_hsat.ma
index 7426d812b..d46e613b4 100644
--- a/matita/matita/lib/pts_dummy/rc_hsat.ma
+++ b/matita/matita/lib/pts_dummy/rc_hsat.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/rc_sat.ma".
-
+include "pts_dummy/rc_sat.ma".
+(*
 (* HIGHER ORDER REDUCIBILITY CANDIDATES ***************************************)
 
 (* An arity is a type of λ→ to be used as carrier for a h.o. r.c. *)
@@ -61,3 +61,4 @@ qed.
 lemma reflexive_defHRC: ∀P. defHRC P ≅^P defHRC P.
 #P (elim P) -P (normalize) /2/
 qed.
+*)
diff --git a/matita/matita/lib/pts_dummy/rc_sat.ma b/matita/matita/lib/pts_dummy/rc_sat.ma
index 3eb04315f..993e3cb36 100644
--- a/matita/matita/lib/pts_dummy/rc_sat.ma
+++ b/matita/matita/lib/pts_dummy/rc_sat.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/sn.ma".
-
+include "pts_dummy/sn.ma".
+(*
 (* REDUCIBILITY CANDIDATES ****************************************************)
 
 (* The reducibility candidate (r.c.) ******************************************)
@@ -179,3 +179,4 @@ qed.
 
 definition lorRC: RC → RC → RC ≝ λB,C. mk_RC (lor_mem B C) ….
 /2/ qed.
+*)
diff --git a/matita/matita/lib/pts_dummy/reduction.ma b/matita/matita/lib/pts_dummy/reduction.ma
index 58e4e179a..66bcd2890 100644
--- a/matita/matita/lib/pts_dummy/reduction.ma
+++ b/matita/matita/lib/pts_dummy/reduction.ma
@@ -9,9 +9,9 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambda/par_reduction.ma".
+include "pts_dummy/par_reduction.ma".
 include "basics/star.ma".
-
+(*
 (*
 inductive T : Type[0] ≝
   | Sort: nat → T
@@ -353,7 +353,4 @@ lemma  SN_APP: ∀P.SN P → ∀N. SN N → ∀M.
    @red_subst1 //
   ]
 qed.
-
-
-
-
+*)
diff --git a/matita/matita/lib/pts_dummy/sn.ma b/matita/matita/lib/pts_dummy/sn.ma
index a9fbff370..193a04e94 100644
--- a/matita/matita/lib/pts_dummy/sn.ma
+++ b/matita/matita/lib/pts_dummy/sn.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/ext_lambda.ma".
-
+include "pts_dummy/ext_lambda.ma".
+(*
 (* STRONGLY NORMALIZING TERMS *************************************************)
 
 (* SN(t) holds when t is strongly normalizing *)
@@ -68,3 +68,4 @@ axiom sn_lambda: ∀N,M. SN N → SN M → SN (Lambda N M).
 axiom sn_prod: ∀N,M. SN N → SN M → SN (Prod N M).
 
 axiom sn_inv_app_1: ∀M,N. SN (App M N) → SN M.
+*)
diff --git a/matita/matita/lib/pts_dummy/subject.ma b/matita/matita/lib/pts_dummy/subject.ma
index be34cb07f..08ac86b48 100644
--- a/matita/matita/lib/pts_dummy/subject.ma
+++ b/matita/matita/lib/pts_dummy/subject.ma
@@ -9,9 +9,9 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambda/reduction.ma".
-include "lambda/inversion.ma". 
-
+include "pts_dummy/reduction.ma".
+include "pts_dummy/inversion.ma". 
+(*
 (*
 inductive T : Type[0] ≝
   | Sort: nat → T
@@ -223,3 +223,4 @@ theorem subject_reduction: ∀P,G,M,N. G ⊢_{P} M:N →
   ]
 qed.
 
+*)
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. 
+*)
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.
+*)
diff --git a/matita/matita/lib/pts_dummy/terms.ma b/matita/matita/lib/pts_dummy/terms.ma
index 554f8099c..dc066c882 100644
--- a/matita/matita/lib/pts_dummy/terms.ma
+++ b/matita/matita/lib/pts_dummy/terms.ma
@@ -9,8 +9,8 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "basics/list.ma".
-include "lambda/lambda_notation.ma".
+include "basics/lists/list.ma".
+include "pts_dummy/lambda_notation.ma".
 
 inductive T : Type[0] ≝
   | Sort: nat → T     (* starts from 0 *)
@@ -30,7 +30,7 @@ let rec Appl F l on l ≝ match l with
    ].
 
 lemma appl_append: ∀N,l,M. Appl M (l @ [N]) = App (Appl M l) N.
-#N #l elim l -l // #hd #tl #IHl #M >IHl //
+#N #l elim l -l // #hd #tl #IHl #M >IHl normalize //
 qed.
 
 (*
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.
+*)
diff --git a/matita/matita/lib/pts_dummy_new/arity.ma b/matita/matita/lib/pts_dummy_new/arity.ma
index 3df7811c0..b5dd81df7 100644
--- a/matita/matita/lib/pts_dummy_new/arity.ma
+++ b/matita/matita/lib/pts_dummy_new/arity.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/ext.ma".
-
+include "pts_dummy/ext.ma".
+(*
 (* ARITIES ********************************************************************)
 
 (* An arity is a normal term representing the functional structure of a term.
@@ -218,3 +218,4 @@ lemma nth_sort_comp: ∀E1,E2. E1 ≅ E2 →
                      ∀i. nth i ? E1 sort ≅ nth i ? E2 sort.
 #E1 #E2 #H #i @(all2_nth … aeq) //
 qed.
+*)
diff --git a/matita/matita/lib/pts_dummy_new/arity_eval.ma b/matita/matita/lib/pts_dummy_new/arity_eval.ma
index 6fcf0e0c0..8adcc4873 100644
--- a/matita/matita/lib/pts_dummy_new/arity_eval.ma
+++ b/matita/matita/lib/pts_dummy_new/arity_eval.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/arity.ma".
-
+include "pts_dummy/arity.ma".
+(*
 (* ARITY ASSIGNMENT ***********************************************************)
 
 (* the arity type *************************************************************)
@@ -226,3 +226,4 @@ axiom cons_comp: ∀a1,a2. a1 ≅ a2 → ∀E1,E2. E1 ≅ E2 → a1 :: E1 ≅ a2
 axiom pippo: ∀A:Type[0]. ∀a,b,c. (a::b) @ c = a :: b @ c.
 @A qed.
 *)
+*)
diff --git a/matita/matita/lib/pts_dummy_new/convertibility.ma b/matita/matita/lib/pts_dummy_new/convertibility.ma
index 377d3c890..23a9c6864 100644
--- a/matita/matita/lib/pts_dummy_new/convertibility.ma
+++ b/matita/matita/lib/pts_dummy_new/convertibility.ma
@@ -9,8 +9,8 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambda/reduction.ma".
-
+include "pts_dummy/reduction.ma".
+(*
 (*
 inductive T : Type[0] ≝
   | Sort: nat → T
@@ -71,3 +71,4 @@ theorem main1: ∀M,N. CO M N →
   |@(ex_intro … M) @(ex_intro … M) % // % //
   ]
 *)
+*)
\ No newline at end of file
diff --git a/matita/matita/lib/pts_dummy_new/cube.ma b/matita/matita/lib/pts_dummy_new/cube.ma
index 8ac3d978c..c143261ad 100644
--- a/matita/matita/lib/pts_dummy_new/cube.ma
+++ b/matita/matita/lib/pts_dummy_new/cube.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "convertibility.ma".
-include "types.ma".
-
+include "pts_dummy/convertibility.ma".
+include "pts_dummy/types.ma".
+(*
 (* PURE TYPE SYSTEMS OF THE λ-CUBE ********************************************)
 
 inductive Cube_Ax: nat → nat → Prop ≝
@@ -41,3 +41,4 @@ inductive FO_Re: nat → nat → nat → Prop ≝
 .
 
 definition FO: pts ≝ mk_pts Cube_Ax FO_Re conv.
+*)
diff --git a/matita/matita/lib/pts_dummy_new/ext.ma b/matita/matita/lib/pts_dummy_new/ext.ma
index 7e64aba31..dcbe395a9 100644
--- a/matita/matita/lib/pts_dummy_new/ext.ma
+++ b/matita/matita/lib/pts_dummy_new/ext.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basics/list.ma".
+include "basics/lists/list.ma".
 
 (* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
 
diff --git a/matita/matita/lib/pts_dummy_new/ext_lambda.ma b/matita/matita/lib/pts_dummy_new/ext_lambda.ma
index a183047e0..fe2587ae8 100644
--- a/matita/matita/lib/pts_dummy_new/ext_lambda.ma
+++ b/matita/matita/lib/pts_dummy_new/ext_lambda.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/ext.ma".
-include "lambda/subst.ma".
-
+include "pts_dummy/ext.ma".
+include "pts_dummy/subst.ma".
+(*
 (* MATTER CONCERNING STRONG NORMALIZATION TO BE PUT ELSEWHERE *****************)
 
 (* substitution ***************************************************************)
@@ -79,3 +79,4 @@ qed.
 
 lemma tsubst_sort: ∀n,l. (Sort n)[/l] = Sort n.
 // qed.
+*)
diff --git a/matita/matita/lib/pts_dummy_new/inversion.ma b/matita/matita/lib/pts_dummy_new/inversion.ma
index 511fa0309..6f1743ce2 100644
--- a/matita/matita/lib/pts_dummy_new/inversion.ma
+++ b/matita/matita/lib/pts_dummy_new/inversion.ma
@@ -9,7 +9,7 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambdaN/thinning.ma".
+include "pts_dummy_new/thinning.ma".
 
 (*
 inductive TJ (p: pts): list T → T → T → Prop ≝
diff --git a/matita/matita/lib/pts_dummy_new/par_reduction.ma b/matita/matita/lib/pts_dummy_new/par_reduction.ma
index 260157d4c..d906160ca 100644
--- a/matita/matita/lib/pts_dummy_new/par_reduction.ma
+++ b/matita/matita/lib/pts_dummy_new/par_reduction.ma
@@ -9,7 +9,7 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambdaN/subterms.ma".
+include "pts_dummy_new/subterms.ma".
 
 (*
 inductive T : Type[0] ≝
@@ -88,7 +88,7 @@ lemma prD: ∀M,N,P. pr (D M N) P →
    @(ex_intro … M2) @(ex_intro … N2) /3/
   ]
 qed.
-
+(* BEGIN HERE
 lemma prApp_not_lambda: 
 ∀M,N,P. pr (App M N) P → is_lambda M = false →
   ∃M1,N1. (P = App M1 N1 ∧ pr M M1 ∧ pr N N1).
@@ -292,4 +292,4 @@ theorem diamond: ∀P,Q,R. pr P Q → pr P R → ∃S.
 pr Q S ∧ pr P S.
 #P #Q #R #pr1 #pr2 @(ex_intro … (full P)) /3/
 qed.
-
+*)
diff --git a/matita/matita/lib/pts_dummy_new/rc_eval.ma b/matita/matita/lib/pts_dummy_new/rc_eval.ma
index 3fdeed410..7b7ce54d9 100644
--- a/matita/matita/lib/pts_dummy_new/rc_eval.ma
+++ b/matita/matita/lib/pts_dummy_new/rc_eval.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/rc_hsat.ma".
-
+include "pts_dummy/rc_hsat.ma".
+(*
 (* THE EVALUATION *************************************************************)
 
 (* The arity of a term t in an environment E *)
diff --git a/matita/matita/lib/pts_dummy_new/rc_hsat.ma b/matita/matita/lib/pts_dummy_new/rc_hsat.ma
index 7426d812b..d46e613b4 100644
--- a/matita/matita/lib/pts_dummy_new/rc_hsat.ma
+++ b/matita/matita/lib/pts_dummy_new/rc_hsat.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/rc_sat.ma".
-
+include "pts_dummy/rc_sat.ma".
+(*
 (* HIGHER ORDER REDUCIBILITY CANDIDATES ***************************************)
 
 (* An arity is a type of λ→ to be used as carrier for a h.o. r.c. *)
@@ -61,3 +61,4 @@ qed.
 lemma reflexive_defHRC: ∀P. defHRC P ≅^P defHRC P.
 #P (elim P) -P (normalize) /2/
 qed.
+*)
diff --git a/matita/matita/lib/pts_dummy_new/rc_sat.ma b/matita/matita/lib/pts_dummy_new/rc_sat.ma
index 3eb04315f..993e3cb36 100644
--- a/matita/matita/lib/pts_dummy_new/rc_sat.ma
+++ b/matita/matita/lib/pts_dummy_new/rc_sat.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/sn.ma".
-
+include "pts_dummy/sn.ma".
+(*
 (* REDUCIBILITY CANDIDATES ****************************************************)
 
 (* The reducibility candidate (r.c.) ******************************************)
@@ -179,3 +179,4 @@ qed.
 
 definition lorRC: RC → RC → RC ≝ λB,C. mk_RC (lor_mem B C) ….
 /2/ qed.
+*)
diff --git a/matita/matita/lib/pts_dummy_new/reduction.ma b/matita/matita/lib/pts_dummy_new/reduction.ma
index 82891b23b..ce3d6cc71 100644
--- a/matita/matita/lib/pts_dummy_new/reduction.ma
+++ b/matita/matita/lib/pts_dummy_new/reduction.ma
@@ -9,7 +9,7 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambdaN/par_reduction.ma".
+include "pts_dummy_new/par_reduction.ma".
 include "basics/star.ma".
 
 (*
@@ -93,9 +93,9 @@ qed.
 
 definition reduct ≝ λn,m. red m n.
 
-definition SN ≝ WF ? reduct.
+definition SN : T → Prop ≝ WF ? reduct.
 
-definition NF ≝ λM. ∀N. ¬ (reduct N M).
+definition NF : T → Prop ≝ λM. ∀N. ¬ (reduct N M).
 
 theorem NF_to_SN: ∀M. NF M → SN M.
 #M #nfM % #a #red @False_ind /2/
@@ -149,13 +149,13 @@ qed.
 lemma star_appl: ∀M,M1,N. star … red M M1 → 
   star … red (App M N) (App M1 N).
 #M #M1 #N #star1 (elim star1) //
-#B #C #starMB #redBC #H @(inj … H) /2/ 
+#B #C #starMB #redBC #H /3 width=3/ 
 qed.
   
 lemma star_appr: ∀M,N,N1. star … red N N1 →
   star … red (App M N) (App M N1).
 #M #N #N1 #star1 (elim star1) // 
-#B #C #starMB #redBC #H @(inj … H) /2/
+#B #C #starMB #redBC #H /3 width=3/
 qed.
  
 lemma star_app: ∀M,M1,N,N1. star … red M M1 → star … red N N1 → 
@@ -166,13 +166,13 @@ qed.
 lemma star_laml: ∀M,M1,N. star … red M M1 → 
   star … red (Lambda M N) (Lambda M1 N).
 #M #M1 #N #star1 (elim star1) //
-#B #C #starMB #redBC #H @(inj … H) /2/ 
+#B #C #starMB #redBC #H /3 width=3/ 
 qed.
   
 lemma star_lamr: ∀M,N,N1. star … red N N1 →
   star … red (Lambda M N) (Lambda M N1).
 #M #N #N1 #star1 (elim star1) //
-#B #C #starMB #redBC #H @(inj … H) /2/
+#B #C #starMB #redBC #H /3 width=3/
 qed.
  
 lemma star_lam: ∀M,M1,N,N1. star … red M M1 → star … red N N1 → 
@@ -183,13 +183,13 @@ qed.
 lemma star_prodl: ∀M,M1,N. star … red M M1 → 
   star … red (Prod M N) (Prod M1 N).
 #M #M1 #N #star1 (elim star1) //
-#B #C #starMB #redBC #H @(inj … H) /2/ 
+#B #C #starMB #redBC #H /3 width=3/
 qed.
   
 lemma star_prodr: ∀M,N,N1. star … red N N1 →
   star … red (Prod M N) (Prod M N1).
 #M #N #N1 #star1 (elim star1) //
-#B #C #starMB #redBC #H @(inj … H) /2/
+#B #C #starMB #redBC #H /3 width=3/
 qed.
  
 lemma star_prod: ∀M,M1,N,N1. star … red M M1 → star … red N N1 → 
@@ -200,13 +200,13 @@ qed.
 lemma star_dl: ∀M,M1,N. star … red M M1 → 
   star … red (D M N) (D M1 N).
 #M #M1 #N #star1 (elim star1) //
-#B #C #starMB #redBC #H @(inj … H) /2/ 
+#B #C #starMB #redBC #H /3 width=3/
 qed.
   
 lemma star_dr: ∀M,N,N1. star … red N N1 →
   star … red (D M N) (D M N1).
 #M #N #N1 #star1 (elim star1) //
-#B #C #starMB #redBC #H @(inj … H) /2/
+#B #C #starMB #redBC #H /3 width=3/
 qed.
 
 lemma star_d: ∀M,M1,N,N1. star … red M M1 → star … red N N1 → 
@@ -357,8 +357,8 @@ lemma  SN_APP: ∀P.SN P → ∀N. SN N → ∀M.
 #P #snP (elim snP) #A #snA #HindA
 #N #snN (elim snN) #B #snB #HindB
 #M #snM1 (cut (SH M)) [@SN_to_SH @(SN_subst … snM1)] #shM 
-(generalize in match snM1) (elim shM)
-#C #shC #HindC #snC1 % #Q #redQ (cases (red_app … redQ))
+generalize in match snM1; elim shM
+#C #shC #HindC #snC1 % #Q #redQ cases (red_app … redQ);
   [*
     [* #M2 * #N2 * #eqlam destruct #eqQ //
     |* #M2 * #eqQ #redlam >eqQ (cases (red_lambda …redlam))
diff --git a/matita/matita/lib/pts_dummy_new/sn.ma b/matita/matita/lib/pts_dummy_new/sn.ma
index a9fbff370..193a04e94 100644
--- a/matita/matita/lib/pts_dummy_new/sn.ma
+++ b/matita/matita/lib/pts_dummy_new/sn.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "lambda/ext_lambda.ma".
-
+include "pts_dummy/ext_lambda.ma".
+(*
 (* STRONGLY NORMALIZING TERMS *************************************************)
 
 (* SN(t) holds when t is strongly normalizing *)
@@ -68,3 +68,4 @@ axiom sn_lambda: ∀N,M. SN N → SN M → SN (Lambda N M).
 axiom sn_prod: ∀N,M. SN N → SN M → SN (Prod N M).
 
 axiom sn_inv_app_1: ∀M,N. SN (App M N) → SN M.
+*)
diff --git a/matita/matita/lib/pts_dummy_new/subject.ma b/matita/matita/lib/pts_dummy_new/subject.ma
index e33364f6b..57619eba6 100644
--- a/matita/matita/lib/pts_dummy_new/subject.ma
+++ b/matita/matita/lib/pts_dummy_new/subject.ma
@@ -9,8 +9,8 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambdaN/reduction.ma".
-include "lambdaN/inversion.ma". 
+include "pts_dummy_new/reduction.ma".
+include "pts_dummy_new/inversion.ma". 
 
 (*
 inductive T : Type[0] ≝
@@ -51,7 +51,7 @@ theorem type_of_type: ∀P,G,A,B. G ⊢_{P} A : B → (∀i. B ≠ Sort i) →
   |#G1 #A #i #t1 #_ #P @(ex_intro … i) @(weak … t1 t1)
   |#G1 #A #B #C #i #t1 #t2 #H1 #H2 #H3 (cases (H1 ?) )
     [#i #Bi @(ex_intro … i) @(weak … Bi t2)
-    |#i @(not_to_not … (H3 i)) //
+    |#i @(not_to_not … (H3 i)) /2 width=2/
     ]
   |#G1 #A #B #i #j #k #h #t1 #t2 #_ #_ #H3 @False_ind /2/
   |#G1 #A #B #C #D #t1 #t2 #H1 #H2 #H3 cases (H1 ?);
diff --git a/matita/matita/lib/pts_dummy_new/subst.ma b/matita/matita/lib/pts_dummy_new/subst.ma
index 225316e81..469691073 100644
--- a/matita/matita/lib/pts_dummy_new/subst.ma
+++ b/matita/matita/lib/pts_dummy_new/subst.ma
@@ -9,7 +9,10 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambdaN/terms.ma".
+include "pts_dummy_new/terms.ma".
+
+(* to be put elsewhere *)
+definition if_then_else ≝ λT:Type[0].λe,t,f.match e return λ_.T with [ true ⇒ t | false ⇒ f].
 
 (* arguments: k is the depth (starts from 0), p is the height (starts from 0) *)
 let rec lift t k p ≝
@@ -129,7 +132,7 @@ nnormalize; //; nqed. *)
 lemma subst_lift_k: ∀A,B.∀k. (lift B k 1)[k ≝ A] = B.
 #A #B (elim B) normalize /2/ #n #k
 @(leb_elim k n) normalize #Hnk
-  [cut (k ≤ n+1) [@transitive_le //] #H
+  [cut (k ≤ n+1); [@transitive_le //] #H
    >(le_to_leb_true … H) normalize 
    >(not_eq_to_eqb_false k (n+1)) normalize /2/
   |>(lt_to_leb_false … (not_le_to_lt … Hnk)) normalize //
@@ -237,7 +240,7 @@ theorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k →
   [2,3,4,5: #T #T0 #Hind1 #Hind2 #i #j #k #leij #lejk
    @eq_f2 /2/ @Hind2 (applyS (monotonic_le_plus_l 1)) //
   |#n #i #j #k #leij #ltjk @(leb_elim i n) normalize #len
-    [cut (j < n + S k)
+    [cut (j < n + S k);
       [<plus_n_Sm @le_S_S @(transitive_le … ltjk) /2/] #H
      >(le_to_leb_true j (n+S k));
       [normalize >(not_eq_to_eqb_false j (n+S k)) normalize /2/ 
@@ -267,7 +270,7 @@ lemma subst_lemma: ∀A,B,C.∀k,i.
         [cut (k+i+1 = n); [/2/] #H1
          >(le_to_leb_true (k+i+1) n) /2/
          >(eq_to_eqb_true … H1) normalize 
-         (generalize in match ltin)
+         generalize in match ltin;
          @(lt_O_n_elim … posn) #m #leim >delift // /2/ 
         |(cut (k+i < n-1)) [@not_eq_to_le_to_lt; //] #Hlt 
          >(le_to_leb_true (k+i+1) n); 
diff --git a/matita/matita/lib/pts_dummy_new/subterms.ma b/matita/matita/lib/pts_dummy_new/subterms.ma
index 86a8507ed..bc7fa2a05 100644
--- a/matita/matita/lib/pts_dummy_new/subterms.ma
+++ b/matita/matita/lib/pts_dummy_new/subterms.ma
@@ -9,7 +9,7 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambdaN/subst.ma".
+include "pts_dummy_new/subst.ma".
 
 inductive subterm : T → T → Prop ≝
   | appl : ∀M,N. subterm M (App M N)
diff --git a/matita/matita/lib/pts_dummy_new/terms.ma b/matita/matita/lib/pts_dummy_new/terms.ma
index 0227f1e94..1291013ff 100644
--- a/matita/matita/lib/pts_dummy_new/terms.ma
+++ b/matita/matita/lib/pts_dummy_new/terms.ma
@@ -9,8 +9,8 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "basics/list.ma".
-include "lambda/lambda_notation.ma".
+include "basics/lists/list.ma".
+include "pts_dummy/lambda_notation.ma".
 
 inductive T : Type[0] ≝
   | Sort: nat → T     (* starts from 0 *)
diff --git a/matita/matita/lib/pts_dummy_new/thinning.ma b/matita/matita/lib/pts_dummy_new/thinning.ma
index 1fcd6fe62..b412392d4 100644
--- a/matita/matita/lib/pts_dummy_new/thinning.ma
+++ b/matita/matita/lib/pts_dummy_new/thinning.ma
@@ -9,7 +9,7 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambdaN/types.ma".
+include "pts_dummy_new/types.ma".
 
 (*
 inductive TJ (p: pts): list T → T → T → Prop ≝
@@ -82,14 +82,14 @@ lemma weak_gen: ∀P,E,M,N. E ⊢_{P} M : N →
      #Heq1 <Heq1 @(Hind2 ? (P::D)) normalize //
     ]
   |#G #P #Q #R #S #tjP #tjS #Hind1 #Hind2
-   #G1 #D #A #l #Heq #tjA (normalize in Hind1 ⊢ %)
+   #G1 #D #A #l #Heq #tjA normalize in Hind1 ⊢ %;
    >(lift_subst_up R S 1 0 (length ? D)) @(app … (lift Q (length ? D) 1));
     [@Hind1 // |@Hind2 //]
   |#G #P #Q #R #i #tjR #tjProd #Hind1 #Hind2
    #G1 #D #A #l #Heq #tjA normalize @(abs … i); 
     [cut (∀n. S n = n +1); [//] #H <H 
      @(Hind1 G1 (P::D) … tjA) normalize //
-    |(normalize in Hind2) @(Hind2 …tjA) //
+    | normalize in Hind2; @(Hind2 …tjA) //
     ]
   |#G #P #Q #R #i #convQR #tjP #tjQ #Hind1 #Hind2
    #G1 #D #A #l #Heq #tjA
diff --git a/matita/matita/lib/pts_dummy_new/types.ma b/matita/matita/lib/pts_dummy_new/types.ma
index 7b4417232..92dc4bd3e 100644
--- a/matita/matita/lib/pts_dummy_new/types.ma
+++ b/matita/matita/lib/pts_dummy_new/types.ma
@@ -9,8 +9,8 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "lambdaN/subst.ma".
-include "basics/list.ma".
+include "pts_dummy_new/subst.ma".
+include "basics/lists/list.ma".
 
 
 (*************************** substl *****************************)
@@ -147,8 +147,8 @@ theorem substitution_tj:
     ]
   |#G #A1 #i #tjA #Hind #G1 #D (cases D) 
     [#N #Heq #tjN >(delift (lift N O O) A1 O O O ??) //
-     (normalize in Heq) destruct /2/
-    |#H #L #N1 #Heq (normalize in Heq)
+     normalize in Heq; destruct normalize /2/
+    |#H #L #N1 #Heq normalize in Heq;
      #tjN1 normalize destruct; (applyS start) /2/
     ]
   |#G #P #Q #R #i #tjP #tjR #Hind1 #Hind2 #G1 #D #N
@@ -166,16 +166,16 @@ theorem substitution_tj:
      #Heq1 <Heq1 @(Hind2 ? (P::D)) normalize //
     ]
   |#G #P #Q #R #S #tjP #tjS #Hind1 #Hind2
-   #G1 #D #N #Heq #tjN (normalize in Hind1 ⊢ %)
-   >(plus_n_O (length ? D)) in ⊢ (? ? ? ? (? ? % ?))
-   >(subst_lemma R S N ? 0) (applyS app) /2/
+   #G1 #D #N #Heq #tjN normalize in Hind1 ⊢ %;
+   >(plus_n_O (length ? D)) in ⊢ (? ? ? ? (? ? % ?));
+   >(subst_lemma R S N ? 0) applyS app /2/
   |#G #P #Q #R #i #tjR #tjProd #Hind1 #Hind2
    #G1 #D #N #Heq #tjN normalize
    (applyS abs) 
-    [normalize in Hind2 /2/
+    [normalize in Hind2; /2/
     |(* napplyS (Hind1 G1 (P::D) N ? tjN); sistemare *)
      generalize in match (Hind1 G1 (P::D) N ? tjN);
-      [#H (normalize in H) (applyS H) | normalize // ]
+      [#H normalize in H; applyS H | normalize // ]
     ]
   |#G #P #Q #R #i #convQR #tjP #tjQ #Hind1 #Hind2
    #G1 #D #N #Heq #tjN
diff --git a/matita/matita/lib/tutorial/chapter6.ma b/matita/matita/lib/tutorial/chapter6.ma
index d243ce5c0..364ad35de 100644
--- a/matita/matita/lib/tutorial/chapter6.ma
+++ b/matita/matita/lib/tutorial/chapter6.ma
@@ -48,10 +48,7 @@ w1,w2,...wk all belonging to l, such that l = w1w2...wk.
 We need to define the latter operations. The following flatten function takes in 
 input a list of words and concatenates them together. *)
 
-(* FG: flatten in list.ma gets in the way:
-alias id "flatten" = "cic:/matita/tutorial/chapter6/flatten.fix(0,1,4)".
-does not work, so we use flatten in lists for now
-
+(* Already in the library
 let rec flatten (S : DeqSet) (l : list (word S)) on l : word S ≝ 
 match l with [ nil ⇒ [ ] | cons w tl ⇒ w @ flatten ? tl ].
 *)
@@ -161,7 +158,7 @@ qed.
 lemma cat_to_star:∀S.∀A:word S → Prop.
   ∀w1,w2. A w1 → A^* w2 → A^* (w1@w2).
 #S #A #w1 #w2 #Aw * #l * #H #H1 @(ex_intro … (w1::l)) 
-% destruct // normalize /2/
+% normalize destruct /2/ (* destruct added *)
 qed.
 
 lemma fix_star: ∀S.∀A:word S → Prop. 
@@ -170,7 +167,7 @@ lemma fix_star: ∀S.∀A:word S → Prop.
   [* #l generalize in match w; -w cases l [normalize #w * /2/]
    #w1 #tl #w * whd in ⊢ ((??%?)→?); #eqw whd in ⊢ (%→?); *
    #w1A #cw1 %1 @(ex_intro … w1) @(ex_intro … (flatten S tl))
-   % destruct /2/ whd @(ex_intro … tl) /2/
+   % destruct /2/ whd @(ex_intro … tl) /2/ (* destruct added *)
   |* [2: whd in ⊢ (%→?); #eqw <eqw //]
    * #w1 * #w2 * * #eqw <eqw @cat_to_star 
   ]
@@ -197,4 +194,4 @@ lemma star_epsilon: ∀S:DeqSet.∀A:word S → Prop.
   A^* ∪ {ϵ} =1 A^*.
 #S #A #w % /2/ * // 
 qed.
-  
\ No newline at end of file
+  
diff --git a/matita/matita/lib/tutorial/chapter7.ma b/matita/matita/lib/tutorial/chapter7.ma
index 739afb52d..20b670018 100644
--- a/matita/matita/lib/tutorial/chapter7.ma
+++ b/matita/matita/lib/tutorial/chapter7.ma
@@ -120,7 +120,10 @@ let rec forget (S: DeqSet) (l : pitem S) on l: re S ≝
   | pc E1 E2 ⇒ (forget ? E1) · (forget ? E2)
   | po E1 E2 ⇒ (forget ? E1) + (forget ? E2)
   | pk E ⇒ (forget ? E)^* ].
- 
+
+(* Already in the library
+notation "| term 19 C |" with precedence 70 for @{ 'card $C }.
+*)
 interpretation "forget" 'card a = (forget ? a).
 
 lemma erase_dot : ∀S.∀e1,e2:pitem S. |e1 · e2| = c ? (|e1|) (|e2|).
@@ -304,4 +307,4 @@ lemma minus_eps_pre: ∀S.∀e:pre S. \sem{\fst e} =1 \sem{e}-{[ ]}.
     [/3/ | * * // #H1 #H2 @False_ind @(absurd …H1 H2)]
   |>sem_pre_false normalize in ⊢ (??%?); #w % [ /3/ | * // ]
   ]
-qed.
\ No newline at end of file
+qed.