From 87e51ef39b7dc9eaeff2cf319038c8aaca1aeb91 Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 24 Dec 2014 10:02:06 +0000
Subject: [PATCH] removing some old files

---
 .../matita/lib/finite_lambda/finite_lambda.ma | 456 --------------
 .../lib/finite_lambda/finite_lambda_deep.ma   | 562 ------------------
 .../matita/lib/finite_lambda/typing_deep.ma   | 239 --------
 matita/matita/lib/finite_lambda/typing_old.ma | 236 --------
 4 files changed, 1493 deletions(-)
 delete mode 100644 matita/matita/lib/finite_lambda/finite_lambda.ma
 delete mode 100644 matita/matita/lib/finite_lambda/finite_lambda_deep.ma
 delete mode 100644 matita/matita/lib/finite_lambda/typing_deep.ma
 delete mode 100644 matita/matita/lib/finite_lambda/typing_old.ma

diff --git a/matita/matita/lib/finite_lambda/finite_lambda.ma b/matita/matita/lib/finite_lambda/finite_lambda.ma
deleted file mode 100644
index d07960e40..000000000
--- a/matita/matita/lib/finite_lambda/finite_lambda.ma
+++ /dev/null
@@ -1,456 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department of the University of Bologna, Italy.                     
-    ||I||                                                                 
-    ||T||  
-    ||A||  This file is distributed under the terms of the 
-    \   /  GNU General Public License Version 2        
-     \ /      
-      V_______________________________________________________________ *)
-
-include "basics/finset.ma".
-include "basics/star.ma".
-
-
-inductive FType (O:Type[0]): Type[0] ≝
-  | atom : O → FType O 
-  | arrow : FType O → FType O → FType O. 
-
-inductive T (O:Type[0]) (D:O → FinSet): Type[0] ≝
-  | Val: ∀o:O.carr (D o) → T O D        (* a value in a finset *)
-  | Rel: nat → T O D                    (* DB index, base is 0 *)
-  | App: T O D → T O D → T O D          (* function, argument *)
-  | Lambda: FType O → T O D → T O D     (* type, body *)
-  | Vec: FType O → list (T O D) → T O D (* type, body *)
-.
-
-let rec FinSet_of_FType O (D:O→FinSet) (ty:FType O) on ty : FinSet ≝
-  match ty with
-  [atom o ⇒ D o
-  |arrow ty1 ty2 ⇒ FinFun (FinSet_of_FType O D ty1) (FinSet_of_FType O D ty2)
-  ].
-
-(* size *)
-
-let rec size O D (M:T O D) on M ≝
-match M with
-  [Val o a ⇒ 1
-  |Rel n ⇒ 1
-  |App P Q ⇒ size O D P + size O D Q + 1
-  |Lambda Ty P ⇒ size O D P + 1
-  |Vec Ty v ⇒ foldr ?? (λx,a. size O D x + a) 0 v +1
-  ]
-.
-
-(* axiom pos_size: ∀M. 1 ≤ size M. *)
-
-theorem Telim_size: ∀O,D.∀P: T O D → Prop. 
- (∀M. (∀N. size O D N < size O D M → P N) → P M) → ∀M. P M.
-#O #D #P #H #M (cut (∀p,N. size O D N = p → P N))
-  [2: /2/]
-#p @(nat_elim1 p) #m #H1 #N #sizeN @H #N0 #Hlt @(H1 (size O D N0)) //
-qed.
-
-lemma T_elim: 
-  ∀O: Type[0].∀D:O→FinSet.∀P:T O D→Prop.
-  (∀o:O.∀x:D o.P (Val O D o x)) →
-  (∀n:ℕ.P(Rel O D n)) →
-  (∀m,n:T O D.P m→P n→P (App O D m n)) →
-  (∀Ty:FType O.∀m:T O D.P m→P(Lambda O D Ty m)) →
-  (∀Ty:FType O.∀v:list (T O D).
-     (∀x:T O D. mem ? x v → P x) → P(Vec O D Ty v)) →
-  ∀x:T O D.P x.
-#O #D #P #Hval #Hrel #Happ #Hlam #Hvec @Telim_size #x cases x //
-  [ (* app *) #m #n #Hind @Happ @Hind // /2 by le_minus_to_plus/
-  | (* lam *) #ty #m #Hind @Hlam @Hind normalize // 
-  | (* vec *) #ty #v #Hind @Hvec #x lapply Hind elim v
-    [#Hind normalize *
-    |#hd #tl #Hind1 #Hind2 * 
-      [#Hx >Hx @Hind2 normalize //
-      |@Hind1 #N #H @Hind2 @(lt_to_le_to_lt … H) normalize //
-      ]
-    ]
-  ]
-qed.
-       
-        
-(* arguments: k is the nesting depth (starts from 0), p is the lift *)
-let rec lift O D t k p on t ≝ 
-  match t with 
-    [ Val o a ⇒ Val O D o a
-    | Rel n ⇒ if (leb k n) then Rel O D (n+p) else Rel O D n
-    | App m n ⇒ App O D (lift O D m k p) (lift O D n k p)
-    | Lambda Ty n ⇒ Lambda O D Ty (lift O D n (S k) p)
-    | Vec Ty v ⇒ Vec O D Ty (map ?? (λx. lift O D x k p) v) 
-    ].
-
-notation "↑ ^ n ( M )" non associative with precedence 40 for @{'Lift 0 $n $M}.
-notation "↑ _ k ^ n ( M )" non associative with precedence 40 for @{'Lift $n $k $M}.
-
-interpretation "Lift" 'Lift n k M = (lift ?? M k n). 
-
-let rec subst O D t k s on t ≝ 
-  match t with 
-    [ Val o a ⇒ Val O D o a 
-    | Rel n ⇒ if (leb k n) then
-        (if (eqb k n) then lift O D s 0 n else Rel O D (n-1)) 
-        else(Rel O D n)
-    | App m n ⇒ App O D (subst O D m k s) (subst O D n k s)
-    | Lambda T n ⇒ Lambda O D T (subst O D n (S k) s)
-    | Vec T v ⇒ Vec O D T (map ?? (λx. subst O D x k s) v) 
-    ].
-    
-(* notation "hvbox(M break [ k ≝ N ])" 
-   non associative with precedence 90
-   for @{'Subst1 $M $k $N}. *)
- 
-interpretation "Subst" 'Subst1 M k N = (subst M k N). 
-
-(* closed terms ????
-let rec closed_k O D (t: T O D) k on t ≝ 
-  match t with 
-    [ Val o a ⇒ True
-    | Rel n ⇒ n < k 
-    | App m n ⇒ (closed_k O D m k) ∧ (closed_k O D n k)
-    | Lambda T n ⇒ closed_k O D n (k+1)
-    | Vec T v ⇒ closed_list O D v k
-    ]
-    
-and closed_list O D (l: list (T O D)) k on l ≝
-  match l with
-    [ nil ⇒ True
-    | cons hd tl ⇒ closed_k O D hd k ∧ closed_list O D tl k
-    ]
-. *)
-
-inductive is_closed (O:Type[0]) (D:O→FinSet): nat → T O D → Prop ≝
-| cval : ∀k,o,a.is_closed O D k (Val O D o a)
-| cval : ∀k,n. n < k → is_closed O D k (Rel O D n)
-| capp : ∀k,n,m. is_closed O D k m → is_closed O D k n → 
-           is_closed O D k (App O D m n)
-| clam : ∀T,k,m. is_closed O D (k+1) m → is_closed O D k (Lambda O D T m)
-| cvec:  ∀T,k,v. (∀m. mem ? m v → is_closed O D k m) → 
-           is_closed O D k (Vec O D T v).
-           
-lemma is_closed_rel: ∀O,D,n,k.
-  is_closed O D k (Rel O D n) → n < k.
-#O #D #n #k #H inversion H 
-  [#k0 #o #a #eqk #H destruct
-  |#k0 #n0 #ltn0 #eqk #H destruct //
-  |#k0 #M #N #_ #_ #_ #H destruct
-  |#T #k0 #M #_ #_ #H destruct
-  |#T #k0 #v #_ #_ #H destruct
-  ]
-qed.
-                                   
-
-(*** properties of lift and subst ***)
-
-lemma lift_0: ∀O,D.∀t:T O D.∀k. lift O D t k 0 = t.
-#O #D #t @(T_elim … t) normalize // 
-  [#n #k cases (leb k n) normalize // 
-  |#o #v #Hind #k @eq_f lapply Hind -Hind elim v // 
-   #hd #tl #Hind #Hind1 normalize @eq_f2 
-    [@Hind1 %1 //|@Hind #x #Hx @Hind1 %2 //]
-  ]
-qed.
-
-axiom lift_closed: ∀O,D.∀t:T O D.∀k,p. 
-  is_closed O D 0 t → lift O D t k p = t.
-(*
-#O #D #t @(T_elim … t) normalize // 
-  [#n #k normalize // 
-  |#o #v #Hind #k @eq_f lapply Hind -Hind elim v // 
-   #hd #tl #Hind #Hind1 normalize @eq_f2 
-    [@Hind1 %1 //|@Hind #x #Hx @Hind1 %2 //]
-  ]
-qed. *)
-
-let rec to_T O D ty on ty: FinSet_of_FType O D ty → T O D ≝ 
-  match ty return (λty.FinSet_of_FType O D ty → T O D) with 
-  [atom o ⇒ λa.Val O D o a
-  |arrow ty1 ty2 ⇒ λa:FinFun ??.Vec O D ty1  
-    (map ((FinSet_of_FType O D ty1)×(FinSet_of_FType O D ty2)) 
-     (T O D) (λp.to_T O D ty2 (snd … p)) (pi1 … a))
-  ]
-.
-
-axiom inj_to_T: ∀O,D,ty,a1,a2. to_T O D ty a1 = to_T O D ty a2 → a1 = a2.
-
-let rec assoc (A:FinSet) (B:Type[0]) (a:A) l1 l2 on l1 : option B ≝
-  match l1 with
-  [ nil ⇒  None ?
-  | cons hd1 tl1 ⇒ match l2 with
-    [ nil ⇒ None ?
-    | cons hd2 tl2 ⇒ if a==hd1 then Some ? hd2 else assoc A B a tl1 tl2
-    ]
-  ]. 
-  
-lemma same_assoc: ∀A,B,a,l1,v1,v2,N,N1.
-  assoc A B a l1 (v1@N::v2) = Some ? N ∧ assoc A B a l1 (v1@N1::v2) = Some ? N1 
-   ∨ assoc A B a l1 (v1@N::v2) = assoc A B a l1 (v1@N1::v2).
-#A #B #a #l1 #v1 #v2 #N #N1 lapply v1 -v1 elim l1 
-  [#v1 %2 // |#hd #tl #Hind * normalize cases (a==hd) normalize /3/]
-qed.
-
-lemma assoc_to_mem: ∀A,B,a,l1,l2,b. 
-  assoc A B a l1 l2 = Some ? b → mem ? b l2.
-#A #B #a #l1 elim l1
-  [#l2 #b normalize #H destruct
-  |#hd1 #tl1 #Hind * 
-    [#b normalize #H destruct
-    |#hd2 #tl2 #b normalize cases (a==hd1) normalize
-      [#H %1 destruct //|#H %2 @Hind @H]
-    ]
-  ]
-qed.
-
-inductive red (O:Type[0]) (D:O→FinSet) : T O D  →T O D → Prop ≝
-  | rbeta: ∀P,M,N. red O D (App O D (Lambda O D P M) N) (subst O D M 0 N)
-  | riota: ∀ty,v,a,M. 
-      assoc (FinSet_of_FType O D ty) ? a (enum (FinSet_of_FType O D ty)) v = Some ? M →
-      red O D (App O D (Vec O D ty v) (to_T O D ty a)) M
-  | rappl: ∀M,M1,N. red O D M M1 → red O D (App O D M N) (App O D M1 N)
-  | rappr: ∀M,N,N1. red O D N N1 → red O D (App O D M N) (App O D M N1)
-  | rmem: ∀ty,M. red O D (Lambda O D ty M)
-      (Vec O D ty (map ?? (λa. subst O D M 0 (to_T O D ty a)) 
-      (enum (FinSet_of_FType O D ty)))) 
-  | rvec: ∀ty,N,N1,v,v1. red O D N N1 → 
-      red O D (Vec O D ty (v@N::v1)) (Vec O D ty (v@N1::v1)).
- 
-(* some inversion cases *)
-lemma red_vec: ∀O,D,ty,v,M.
-  red O D (Vec O D ty v) M → ∃N,N1,v1,v2.
-      red O D N N1 ∧ v = v1@N::v2 ∧ M = Vec O D ty (v1@N1::v2).
-#O #D #ty #v #M #Hred inversion Hred
-  [#ty1 #M0 #N #H destruct
-  |#ty1 #v1 #a #M0 #_ #H destruct
-  |#M0 #M1 #N #_ #_ #H destruct
-  |#M0 #M1 #N #_ #_ #H destruct
-  |#ty1 #M0 #H destruct
-  |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct #_ %{N} %{N1} %{v1} %{v2} /3/
-  ]
-qed.
-      
-lemma red_lambda: ∀O,D,ty,M,N.
-  red O D (Lambda O D ty M) N → 
-      N = Vec O D ty (map ?? (λa. subst O D M 0 (to_T O D ty a)) 
-      (enum (FinSet_of_FType O D ty))).
-#O #D #ty #M #N #Hred inversion Hred
-  [#ty1 #M0 #N #H destruct
-  |#ty1 #v1 #a #M0 #_ #H destruct
-  |#M0 #M1 #N #_ #_ #H destruct
-  |#M0 #M1 #N #_ #_ #H destruct
-  |#ty1 #M0 #H destruct #_ //
-  |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct
-  ]
-qed. 
-
-lemma red_val: ∀O,D,ty,a,N.
-  red O D (Val O D ty a) N → False.
-#O #D #ty #M #N #Hred inversion Hred
-  [#ty1 #M0 #N #H destruct
-  |#ty1 #v1 #a #M0 #_ #H destruct
-  |#M0 #M1 #N #_ #_ #H destruct
-  |#M0 #M1 #N #_ #_ #H destruct
-  |#ty1 #M0 #H destruct #_ 
-  |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct
-  ]
-qed. 
-
-lemma red_rel: ∀O,D,n,N.
-  red O D (Rel O D n) N → False.
-#O #D #n #N #Hred inversion Hred
-  [#ty1 #M0 #N #H destruct
-  |#ty1 #v1 #a #M0 #_ #H destruct
-  |#M0 #M1 #N #_ #_ #H destruct
-  |#M0 #M1 #N #_ #_ #H destruct
-  |#ty1 #M0 #H destruct #_ 
-  |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct
-  ]
-qed. 
- 
-lemma star_red_appl: ∀O,D,M,M1,N. star ? (red O D) M M1 → 
-  star ? (red O D) (App O D M N) (App O D M1 N).
-#O #D #M #N #N1 #H elim H // 
-#P #Q #Hind #HPQ #Happ %1[|@Happ] @rappl @HPQ
-qed.
-
-lemma star_red_appr: ∀O,D,M,N,N1. star ? (red O D) N N1 → 
-  star ? (red O D) (App O D M N) (App O D M N1).
-#O #D #M #N #N1 #H elim H // 
-#P #Q #Hind #HPQ #Happ %1[|@Happ] @rappr @HPQ
-qed.
-
-lemma star_red_vec: ∀O,D,ty,N,N1,v1,v2. star ? (red O D) N N1 → 
-  star ? (red O D) (Vec O D ty (v1@N::v2)) (Vec O D ty (v1@N1::v2)).
-#O #D #ty #N #N1 #v1 #v2 #H elim H // 
-#P #Q #Hind #HPQ #Hvec %1[|@Hvec] @rvec @HPQ
-qed.
-
-axiom red_subst : ∀O,D,M,N,N1,i. 
-  red O D N N1 → red O D (subst O D M i N) (subst O D M i N1).
-  
-axiom red_star_subst : ∀O,D,M,N,N1,i. 
-  star ? (red O D) N N1 → star ? (red O D) (subst O D M i N) (subst O D M i N1).
-
-axiom canonical_to_T: ∀O,D.∀M:T O D.∀ty.(* type_of M ty → *)
-  ∃a:FinSet_of_FType O D ty. star ? (red O D) M (to_T O D ty a).
-   
-axiom normal_to_T: ∀O,D,M,ty,a. red O D (to_T O D ty a) M → False.
-
-lemma critical: ∀O,D,ty,M,N. 
-  ∃M3:T O D
-  .star (T O D) (red O D) (subst O D M 0 N) M3
-   ∧star (T O D) (red O D)
-    (App O D
-     (Vec O D ty
-      (map (FinSet_of_FType O D ty) (T O D)
-       (λa0:FinSet_of_FType O D ty.subst O D M 0 (to_T O D ty a0))
-       (enum (FinSet_of_FType O D ty)))) N) M3.
-#O #D #ty #M #N
-lapply (canonical_to_T O D N ty) * #a #Ha
-%{(subst O D M 0 (to_T O D ty a))} (* CR-term *)
-%[@red_star_subst @Ha
- |@trans_star [|@(star_red_appr … Ha)] @R_to_star @riota
-  lapply (enum_complete (FinSet_of_FType O D ty) a)
-  elim (enum (FinSet_of_FType O D ty))
-   [normalize #H1 destruct (H1)
-   |#hd #tl #Hind #H cases (orb_true_l … H) -H #Hcase
-     [normalize >Hcase >(\P Hcase) //
-     |normalize cases (true_or_false (a==hd)) #Hcase1
-       [normalize >Hcase1 >(\P Hcase1) // |>Hcase1 @Hind @Hcase]
-     ]
-   ]
- ]
-qed.
-
-lemma critical2: ∀O,D,ty,a,M,M1,M2,v.
-  red O D (Vec O D ty v) M →
-  red O D (App O D (Vec O D ty v) (to_T O D ty a)) M1 →
-  assoc (FinSet_of_FType O D ty) (T O D) a (enum (FinSet_of_FType O D ty)) v
-    =Some (T O D) M2 →
-  ∃M3:T O D
-  .star (T O D) (red O D) M2 M3
-   ∧star (T O D) (red O D) (App O D M (to_T O D ty a)) M3.
-#O #D #ty #a #M #M1 #M2 #v #redM #redM1 #Ha lapply (red_vec … redM) -redM
-* #N * #N1 * #v1 * #v2 * * #Hred1 #Hv #HM0 >HM0 -HM0 >Hv in Ha; #Ha
-cases (same_assoc … a (enum (FinSet_of_FType O D ty)) v1 v2 N N1)
-  [* >Ha -Ha #H1 destruct (H1) #Ha
-   %{N1} (* CR-term *) % [@R_to_star //|@R_to_star @(riota … Ha)]
-  |#Ha1 %{M2} (* CR-term *) % [// | @R_to_star @riota <Ha1 @Ha]
-  ]
-qed.
-
-(* we need to proceed by structural induction on the term and then
-by inversion on the two redexes. The problem are the moves in a 
-same subterm, since we need an induction hypothesis, there *)
-
-lemma local_confluence: ∀O,D,M,M1,M2. red O D M M1 → red O D M M2 → 
-∃M3. star ? (red O D) M1 M3 ∧ star ? (red O D) M2 M3. 
-#O #D #M @(T_elim … M)
-  [#o #a #M1 #M2 #H elim(red_val ????? H)
-  |#n #M1 #M2 #H elim(red_rel ???? H)
-  |(* app : this is the interesting case *)
-   #P #Q #HindP #HindQ
-   #M1 #M2 #H1 inversion H1 -H1
-    [(* right redex is beta *)
-     #ty #Q #N #HM >HM -HM #HM1 >HM1 - HM1 #Hl inversion Hl
-      [#P1 #M1 #N1 #H1 destruct (H1) #H_ %{(subst O D M1 0 N1)} (* CR-term *) /2/
-      |#ty #v #a #M0 #_ #H1 destruct (H1) (* vacuous *)
-      |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #_ inversion redM0
-        [#P0 #M0 #N #H destruct
-        |#ty #v #a #M0 #_ #H1 destruct (H1)
-        |#M0 #M1 #N #_ #_ #H1 destruct (H1)
-        |#M0 #M1 #N #_ #_ #H1 destruct (H1)
-        |#ty1 #M0 #H1 destruct (H1) #HM1 @critical
-        |#ty #N #N1 #v #v1 #_ #_ #H1 destruct (H1)
-        ]
-      |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) #HM2
-       %{(subst O D Q 0 N1)} (* CR-term *) 
-       %[@red_star_subst @R_to_star //|@R_to_star @rbeta]
-      |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
-      |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
-      ]
-    |(* right redex is iota *)#ty #v #a #M3 #Ha #_ #_ #Hl inversion Hl
-      [#P1 #M1 #N1 #H1 destruct (H1) (* vacuous *)
-      |#ty1 #v1 #a1 #M4 #Ha1 #H1 destruct (H1) -H1 #HM4 >(inj_to_T … e0) in Ha;
-       >Ha1 #H1 destruct (H1) %{M3} (* CR-term *) /2/
-      |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2 @(critical2 … redM0 Hl Ha)
-      |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) elim (normal_to_T … redN0N1)
-      |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
-      |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
-      ]
-    |(* right redex is appl *)#M3 #M4 #N #redM3M4 #_ #H1 destruct (H1) #_ 
-      #Hl inversion Hl
-      [#ty1 #M1 #N1 #H1 destruct (H1) #HM2 lapply (red_lambda … redM3M4)
-       #H >H -H lapply (critical O D ty1 M1 N1) * #M3 * #H1 #H2 
-       %{M3} /2/
-      |#ty1 #v1 #a1 #M4 #Ha1 #H1 #H2 destruct 
-       lapply (critical2 … redM3M4 Hl Ha1) * #M3 * #H1 #H2 %{M3} /2/
-      |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2 
-       lapply (HindP … redM0 redM3M4) * #M3 * #H1 #H2 
-       %{(App O D M3 N0)} (* CR-term *) % [@star_red_appl //|@star_red_appl //]
-      |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) #_
-       %{(App O D M4 N1)} % @R_to_star [@rappr //|@rappl //]
-      |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
-      |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
-      ]
-    |(* right redex is appr *)#M3 #N #N1 #redN #_ #H1 destruct (H1) #_ 
-      #Hl inversion Hl
-      [#ty1 #M0 #N0 #H1 destruct (H1) #HM2 
-       %{(subst O D M0 0 N1)} (* CR-term *) % 
-        [@R_to_star @rbeta | @red_star_subst @R_to_star //]
-      |#ty1 #v1 #a1 #M4 #Ha1 #H1 #H2 destruct (H1) elim (normal_to_T … redN)
-      |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2 
-       %{(App O D M10 N1)} (* CR-term *) % @R_to_star [@rappl //|@rappr //]
-      |#M0 #N0 #N10 #redN0 #_ #H1 destruct (H1) #_
-       lapply (HindQ … redN0 redN) * #M3 * #H1 #H2 
-       %{(App O D M0 M3)} (* CR-term *) % [@star_red_appr //|@star_red_appr //]
-      |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
-      |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
-      ]
-    |(* right redex is rmem *) #ty #M0 #H1 destruct (H1) (* vacuous *)
-    |(* right redex is vec *) #ty #N #N1 #v #v1 #_ #_ 
-     #H1 destruct (H1) (* vacuous *)
-    ]
-  |#ty #M1 #Hind #M2 #M3 #H1 #H2  
-   lapply (red_lambda … H1) #HM2 lapply (red_lambda … H2) #HM3
-   %{M2} (* CR-term *) % //
-  |#ty #v1 #Hind #M1 #M2 #H1 #H2
-   lapply (red_vec … H1) * #N11 * #N12 * #v11 * #v12 * * #redN11 #Hv1 #HM1
-   lapply (red_vec … H2) * #N21* #N22 * #v21 * #v22 * * #redN21 #Hv2 #HM2
-   >Hv1 in Hv2; #Hvv lapply (compare_append … Hvv) -Hvv * 
-   (* we must proceed by cases on the list *) * normalize
-    [(* N11 = N21 *) *
-      [>append_nil * #Hl1 #Hl2 destruct lapply(Hind N11 … redN11 redN21)
-        [@mem_append_l2 %1 //]
-       * #M3 * #HM31 #HM32
-       %{(Vec O D ty (v21@M3::v12))} (* CR-term *) 
-       % [@star_red_vec //|@star_red_vec //]
-      |>append_nil * #Hl1 #Hl2 destruct lapply(Hind N21 … redN21 redN11)
-        [@mem_append_l2 %1 //]
-       * #M3 * #HM31 #HM32
-       %{(Vec O D ty (v11@M3::v22))} (* CR-term *) 
-       % [@star_red_vec //|@star_red_vec //]
-      ]
-    |(* N11 ≠  N21 *) -Hind #P #l *
-      [* #Hv11 #Hv22 destruct
-       %{((Vec O D ty ((v21@N22::l)@N12::v12)))} (* CR-term *) % @R_to_star 
-        [>associative_append >associative_append normalize @rvec //
-        |>append_cons <associative_append <append_cons in ⊢ (???%?); @rvec //
-        ]
-      |* #Hv11 #Hv22 destruct
-       %{((Vec O D ty ((v11@N12::l)@N22::v22)))} (* CR-term *) % @R_to_star 
-        [>append_cons <associative_append <append_cons in ⊢ (???%?); @rvec //
-        |>associative_append >associative_append normalize @rvec //
-        ]
-      ]
-    ]
-  ]
-qed.    
-      
-
-
-
diff --git a/matita/matita/lib/finite_lambda/finite_lambda_deep.ma b/matita/matita/lib/finite_lambda/finite_lambda_deep.ma
deleted file mode 100644
index e2613775d..000000000
--- a/matita/matita/lib/finite_lambda/finite_lambda_deep.ma
+++ /dev/null
@@ -1,562 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department of the University of Bologna, Italy.                     
-    ||I||                                                                 
-    ||T||  
-    ||A||  This file is distributed under the terms of the 
-    \   /  GNU General Public License Version 2        
-     \ /      
-      V_______________________________________________________________ *)
-
-include "basics/finset.ma".
-include "basics/star.ma".
-
-
-inductive FType (O:Type[0]): Type[0] ≝
-  | atom : O → FType O 
-  | arrow : FType O → FType O → FType O. 
-
-inductive T (O:Type[0]) (D:O → FinSet): Type[0] ≝
-  | Val: ∀o:O.carr (D o) → T O D        (* a value in a finset *)
-  | Rel: nat → T O D                    (* DB index, base is 0 *)
-  | App: T O D → T O D → T O D          (* function, argument *)
-  | Lambda: FType O → T O D → T O D     (* type, body *)
-  | Vec: FType O → list (T O D) → T O D (* type, body *)
-.
-
-let rec FinSet_of_FType O (D:O→FinSet) (ty:FType O) on ty : FinSet ≝
-  match ty with
-  [atom o ⇒ D o
-  |arrow ty1 ty2 ⇒ FinFun (FinSet_of_FType O D ty1) (FinSet_of_FType O D ty2)
-  ].
-
-(* size *)
-
-let rec size O D (M:T O D) on M ≝
-match M with
-  [Val o a ⇒ 1
-  |Rel n ⇒ 1
-  |App P Q ⇒ size O D P + size O D Q + 1
-  |Lambda Ty P ⇒ size O D P + 1
-  |Vec Ty v ⇒ foldr ?? (λx,a. size O D x + a) 0 v +1
-  ]
-.
-
-(* axiom pos_size: ∀M. 1 ≤ size M. *)
-
-theorem Telim_size: ∀O,D.∀P: T O D → Prop. 
- (∀M. (∀N. size O D N < size O D M → P N) → P M) → ∀M. P M.
-#O #D #P #H #M (cut (∀p,N. size O D N = p → P N))
-  [2: /2/]
-#p @(nat_elim1 p) #m #H1 #N #sizeN @H #N0 #Hlt @(H1 (size O D N0)) //
-qed.
-
-lemma T_elim: 
-  ∀O: Type[0].∀D:O→FinSet.∀P:T O D→Prop.
-  (∀o:O.∀x:D o.P (Val O D o x)) →
-  (∀n:ℕ.P(Rel O D n)) →
-  (∀m,n:T O D.P m→P n→P (App O D m n)) →
-  (∀Ty:FType O.∀m:T O D.P m→P(Lambda O D Ty m)) →
-  (∀Ty:FType O.∀v:list (T O D).
-     (∀x:T O D. mem ? x v → P x) → P(Vec O D Ty v)) →
-  ∀x:T O D.P x.
-#O #D #P #Hval #Hrel #Happ #Hlam #Hvec @Telim_size #x cases x //
-  [ (* app *) #m #n #Hind @Happ @Hind // /2 by le_minus_to_plus/
-  | (* lam *) #ty #m #Hind @Hlam @Hind normalize // 
-  | (* vec *) #ty #v #Hind @Hvec #x lapply Hind elim v
-    [#Hind normalize *
-    |#hd #tl #Hind1 #Hind2 * 
-      [#Hx >Hx @Hind2 normalize //
-      |@Hind1 #N #H @Hind2 @(lt_to_le_to_lt … H) normalize //
-      ]
-    ]
-  ]
-qed.
-       
-        
-(* arguments: k is the nesting depth (starts from 0), p is the lift *)
-let rec lift O D t k p on t ≝ 
-  match t with 
-    [ Val o a ⇒ Val O D o a
-    | Rel n ⇒ if (leb k n) then Rel O D (n+p) else Rel O D n
-    | App m n ⇒ App O D (lift O D m k p) (lift O D n k p)
-    | Lambda Ty n ⇒ Lambda O D Ty (lift O D n (S k) p)
-    | Vec Ty v ⇒ Vec O D Ty (map ?? (λx. lift O D x k p) v) 
-    ].
-
-notation "↑ ^ n ( M )" non associative with precedence 40 for @{'Lift 0 $n $M}.
-notation "↑ _ k ^ n ( M )" non associative with precedence 40 for @{'Lift $n $k $M}.
-
-interpretation "Lift" 'Lift n k M = (lift ?? M k n). 
-
-let rec subst O D t k s on t ≝ 
-  match t with 
-    [ Val o a ⇒ Val O D o a 
-    | Rel n ⇒ if (leb k n) then
-        (if (eqb k n) then lift O D s 0 n else Rel O D (n-1)) 
-        else(Rel O D n)
-    | App m n ⇒ App O D (subst O D m k s) (subst O D n k s)
-    | Lambda T n ⇒ Lambda O D T (subst O D n (S k) s)
-    | Vec T v ⇒ Vec O D T (map ?? (λx. subst O D x k s) v) 
-    ].
-    
-(* notation "hvbox(M break [ k ≝ N ])" 
-   non associative with precedence 90
-   for @{'Subst1 $M $k $N}. *)
- 
-interpretation "Subst" 'Subst1 M k N = (subst M k N). 
-
-(* closed terms ????
-let rec closed_k O D (t: T O D) k on t ≝ 
-  match t with 
-    [ Val o a ⇒ True
-    | Rel n ⇒ n < k 
-    | App m n ⇒ (closed_k O D m k) ∧ (closed_k O D n k)
-    | Lambda T n ⇒ closed_k O D n (k+1)
-    | Vec T v ⇒ closed_list O D v k
-    ]
-    
-and closed_list O D (l: list (T O D)) k on l ≝
-  match l with
-    [ nil ⇒ True
-    | cons hd tl ⇒ closed_k O D hd k ∧ closed_list O D tl k
-    ]
-. *)
-
-inductive is_closed (O:Type[0]) (D:O→FinSet): nat → T O D → Prop ≝
-| cval : ∀k,o,a.is_closed O D k (Val O D o a)
-| cval : ∀k,n. n < k → is_closed O D k (Rel O D n)
-| capp : ∀k,n,m. is_closed O D k m → is_closed O D k n → 
-           is_closed O D k (App O D m n)
-| clam : ∀T,k,m. is_closed O D (k+1) m → is_closed O D k (Lambda O D T m)
-| cvec:  ∀T,k,v. (∀m. mem ? m v → is_closed O D k m) → 
-           is_closed O D k (Vec O D T v).
-           
-lemma is_closed_rel: ∀O,D,n,k.
-  is_closed O D k (Rel O D n) → n < k.
-#O #D #n #k #H inversion H 
-  [#k0 #o #a #eqk #H destruct
-  |#k0 #n0 #ltn0 #eqk #H destruct //
-  |#k0 #M #N #_ #_ #_ #H destruct
-  |#T #k0 #M #_ #_ #H destruct
-  |#T #k0 #v #_ #_ #H destruct
-  ]
-qed.
-                                   
-
-(*** properties of lift and subst ***)
-
-lemma lift_0: ∀O,D.∀t:T O D.∀k. lift O D t k 0 = t.
-#O #D #t @(T_elim … t) normalize // 
-  [#n #k cases (leb k n) normalize // 
-  |#o #v #Hind #k @eq_f lapply Hind -Hind elim v // 
-   #hd #tl #Hind #Hind1 normalize @eq_f2 
-    [@Hind1 %1 //|@Hind #x #Hx @Hind1 %2 //]
-  ]
-qed.
-
-axiom lift_closed: ∀O,D.∀t:T O D.∀k,p. 
-  is_closed O D 0 t → lift O D t k p = t.
-(*
-#O #D #t @(T_elim … t) normalize // 
-  [#n #k normalize // 
-  |#o #v #Hind #k @eq_f lapply Hind -Hind elim v // 
-   #hd #tl #Hind #Hind1 normalize @eq_f2 
-    [@Hind1 %1 //|@Hind #x #Hx @Hind1 %2 //]
-  ]
-qed. *)
-
-let rec to_T O D ty on ty: FinSet_of_FType O D ty → T O D ≝ 
-  match ty return (λty.FinSet_of_FType O D ty → T O D) with 
-  [atom o ⇒ λa.Val O D o a
-  |arrow ty1 ty2 ⇒ λa:FinFun ??.Vec O D ty1  
-    (map ((FinSet_of_FType O D ty1)×(FinSet_of_FType O D ty2)) 
-     (T O D) (λp.to_T O D ty2 (snd … p)) (pi1 … a))
-  ]
-.
-
-axiom inj_to_T: ∀O,D,ty,a1,a2. to_T O D ty a1 = to_T O D ty a2 → a1 = a2.
-
-let rec assoc (A:FinSet) (B:Type[0]) (a:A) l1 l2 on l1 : option B ≝
-  match l1 with
-  [ nil ⇒  None ?
-  | cons hd1 tl1 ⇒ match l2 with
-    [ nil ⇒ None ?
-    | cons hd2 tl2 ⇒ if a==hd1 then Some ? hd2 else assoc A B a tl1 tl2
-    ]
-  ]. 
-  
-lemma same_assoc: ∀A,B,a,l1,v1,v2,N,N1.
-  assoc A B a l1 (v1@N::v2) = Some ? N ∧ assoc A B a l1 (v1@N1::v2) = Some ? N1 
-   ∨ assoc A B a l1 (v1@N::v2) = assoc A B a l1 (v1@N1::v2).
-#A #B #a #l1 #v1 #v2 #N #N1 lapply v1 -v1 elim l1 
-  [#v1 %2 // |#hd #tl #Hind * normalize cases (a==hd) normalize /3/]
-qed.
-
-lemma assoc_to_mem: ∀A,B,a,l1,l2,b. 
-  assoc A B a l1 l2 = Some ? b → mem ? b l2.
-#A #B #a #l1 elim l1
-  [#l2 #b normalize #H destruct
-  |#hd1 #tl1 #Hind * 
-    [#b normalize #H destruct
-    |#hd2 #tl2 #b normalize cases (a==hd1) normalize
-      [#H %1 destruct //|#H %2 @Hind @H]
-    ]
-  ]
-qed.
-
-inductive red (O:Type[0]) (D:O→FinSet) : T O D  →T O D → Prop ≝
-  | (* we only allow beta on closed arguments *)
-    rbeta: ∀P,M,N. is_closed O D 0 N →
-      red O D (App O D (Lambda O D P M) N) (subst O D M 0 N)
-  | riota: ∀ty,v,a,M. 
-      assoc (FinSet_of_FType O D ty) ? a (enum (FinSet_of_FType O D ty)) v = Some ? M →
-      red O D (App O D (Vec O D ty v) (to_T O D ty a)) M
-  | rappl: ∀M,M1,N. red O D M M1 → red O D (App O D M N) (App O D M1 N)
-  | rappr: ∀M,N,N1. red O D N N1 → red O D (App O D M N) (App O D M N1)
-  | rlam: ∀ty,N,N1. red O D N N1 → red O D (Lambda O D ty N) (Lambda O D ty N1) 
-  | rmem: ∀ty,M. red O D (Lambda O D ty M)
-      (Vec O D ty (map ?? (λa. subst O D M 0 (to_T O D ty a)) 
-      (enum (FinSet_of_FType O D ty)))) 
-  | rvec: ∀ty,N,N1,v,v1. red O D N N1 → 
-      red O D (Vec O D ty (v@N::v1)) (Vec O D ty (v@N1::v1)).
- 
-(* some inversion cases *)
-lemma red_vec: ∀O,D,ty,v,M.
-  red O D (Vec O D ty v) M → ∃N,N1,v1,v2.
-      red O D N N1 ∧ v = v1@N::v2 ∧ M = Vec O D ty (v1@N1::v2).
-#O #D #ty #v #M #Hred inversion Hred
-  [#ty1 #M0 #N #Hc #H destruct
-  |#ty1 #v1 #a #M0 #_ #H destruct
-  |#M0 #M1 #N #_ #_ #H destruct
-  |#M0 #M1 #N #_ #_ #H destruct
-  |#ty1 #M #M1 #_ #_ #H destruct
-  |#ty1 #M0 #H destruct
-  |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct #_ %{N} %{N1} %{v1} %{v2} /3/
-  ]
-qed.
-      
-lemma red_lambda: ∀O,D,ty,M,N.
-  red O D (Lambda O D ty M) N → 
-      (∃M1. red O D M M1 ∧ N = (Lambda O D ty M1)) ∨
-      N = Vec O D ty (map ?? (λa. subst O D M 0 (to_T O D ty a)) 
-      (enum (FinSet_of_FType O D ty))).
-#O #D #ty #M #N #Hred inversion Hred
-  [#ty1 #M0 #N #Hc #H destruct
-  |#ty1 #v1 #a #M0 #_ #H destruct
-  |#M0 #M1 #N #_ #_ #H destruct
-  |#M0 #M1 #N #_ #_ #H destruct
-  |#ty1 #P #P1 #redP #_ #H #H1 destruct %1 %{P1} % //
-  |#ty1 #M0 #H destruct #_ %2 //
-  |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct
-  ]
-qed. 
-
-lemma red_val: ∀O,D,ty,a,N.
-  red O D (Val O D ty a) N → False.
-#O #D #ty #M #N #Hred inversion Hred
-  [#ty1 #M0 #N #Hc #H destruct
-  |#ty1 #v1 #a #M0 #_ #H destruct
-  |#M0 #M1 #N #_ #_ #H destruct
-  |#M0 #M1 #N #_ #_ #H destruct
-  |#ty1 #N1 #N2 #_ #_ #H destruct
-  |#ty1 #M0 #H destruct #_ 
-  |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct
-  ]
-qed. 
-
-lemma red_rel: ∀O,D,n,N.
-  red O D (Rel O D n) N → False.
-#O #D #n #N #Hred inversion Hred
-  [#ty1 #M0 #N #Hc #H destruct
-  |#ty1 #v1 #a #M0 #_ #H destruct
-  |#M0 #M1 #N #_ #_ #H destruct
-  |#M0 #M1 #N #_ #_ #H destruct
-  |#ty1 #N1 #N2 #_ #_ #H destruct
-  |#ty1 #M0 #H destruct #_ 
-  |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct
-  ]
-qed. 
- 
-lemma star_red_appl: ∀O,D,M,M1,N. star ? (red O D) M M1 → 
-  star ? (red O D) (App O D M N) (App O D M1 N).
-#O #D #M #N #N1 #H elim H // 
-#P #Q #Hind #HPQ #Happ %1[|@Happ] @rappl @HPQ
-qed.
-
-lemma star_red_appr: ∀O,D,M,N,N1. star ? (red O D) N N1 → 
-  star ? (red O D) (App O D M N) (App O D M N1).
-#O #D #M #N #N1 #H elim H // 
-#P #Q #Hind #HPQ #Happ %1[|@Happ] @rappr @HPQ
-qed.
-
-lemma star_red_vec: ∀O,D,ty,N,N1,v1,v2. star ? (red O D) N N1 → 
-  star ? (red O D) (Vec O D ty (v1@N::v2)) (Vec O D ty (v1@N1::v2)).
-#O #D #ty #N #N1 #v1 #v2 #H elim H // 
-#P #Q #Hind #HPQ #Hvec %1[|@Hvec] @rvec @HPQ
-qed.
-
-lemma star_red_vec1: ∀O,D,ty,v1,v2,v. |v1| = |v2| →
-  (∀n,M. star ? (red O D) (nth n ? v1 M) (nth n ? v2 M)) → 
-  star ? (red O D) (Vec O D ty (v@v1)) (Vec O D ty (v@v2)).
-#O #D #ty #v1 elim v1 
-  [#v2 #v normalize #Hv2 >(lenght_to_nil … (sym_eq … Hv2)) normalize //
-  |#N1 #tl1 #Hind * [normalize #v #H destruct] #N2 #tl2 #v normalize #HS
-   #H @(trans_star … (Vec O D ty (v@N2::tl1)))
-    [@star_red_vec @(H 0 N1)
-    |>append_cons >(append_cons ??? tl2) @(Hind… (injective_S … HS))
-     #n #M @(H (S n))
-    ]
-  ]
-qed.
-
-lemma star_red_vec2: ∀O,D,ty,v1,v2. |v1| = |v2| →
-  (∀n,M. star ? (red O D) (nth n ? v1 M) (nth n ? v2 M)) → 
-  star ? (red O D) (Vec O D ty v1) (Vec O D ty v2).
-#O #D #ty #v1 #v2 @(star_red_vec1 … [ ])
-qed.
-
-lemma star_red_lambda: ∀O,D,ty,N,N1. star ? (red O D) N N1 → 
-  star ? (red O D) (Lambda O D ty N) (Lambda O D ty N1).
-#O #D #ty #N #N1 #H elim H // 
-#P #Q #Hind #HPQ #Hlam %1[|@Hlam] @rlam @HPQ
-qed.
-
-axiom red_subst : ∀O,D,M,N,N1,i. 
-  red O D N N1 → red O D (subst O D M i N) (subst O D M i N1).
-  
-axiom red_star_subst : ∀O,D,M,N,N1,i. 
-  star ? (red O D) N N1 → star ? (red O D) (subst O D M i N) (subst O D M i N1).
-  
-axiom red_star_subst2 : ∀O,D,M,M1,N,i. 
-  star ? (red O D) M M1 → star ? (red O D) (subst O D M i N) (subst O D M1 i N).
-
-axiom canonical_to_T: ∀O,D.∀M:T O D.∀ty.(* type_of M ty → *)
-  ∃a:FinSet_of_FType O D ty. star ? (red O D) M (to_T O D ty a).
-   
-axiom normal_to_T: ∀O,D,M,ty,a. red O D (to_T O D ty a) M → False.
-
-axiom red_closed: ∀O,D,M,M1. 
-  is_closed O D 0 M → red O D M M1 → is_closed O D 0 M1.
-
-lemma critical: ∀O,D,ty,M,N. 
-  ∃M3:T O D
-  .star (T O D) (red O D) (subst O D M 0 N) M3
-   ∧star (T O D) (red O D)
-    (App O D
-     (Vec O D ty
-      (map (FinSet_of_FType O D ty) (T O D)
-       (λa0:FinSet_of_FType O D ty.subst O D M 0 (to_T O D ty a0))
-       (enum (FinSet_of_FType O D ty)))) N) M3.
-#O #D #ty #M #N
-lapply (canonical_to_T O D N ty) * #a #Ha
-%{(subst O D M 0 (to_T O D ty a))} (* CR-term *)
-%[@red_star_subst @Ha
- |@trans_star [|@(star_red_appr … Ha)] @R_to_star @riota
-  lapply (enum_complete (FinSet_of_FType O D ty) a)
-  elim (enum (FinSet_of_FType O D ty))
-   [normalize #H1 destruct (H1)
-   |#hd #tl #Hind #H cases (orb_true_l … H) -H #Hcase
-     [normalize >Hcase >(\P Hcase) //
-     |normalize cases (true_or_false (a==hd)) #Hcase1
-       [normalize >Hcase1 >(\P Hcase1) // |>Hcase1 @Hind @Hcase]
-     ]
-   ]
- ]
-qed.
-
-lemma critical2: ∀O,D,ty,a,M,M1,M2,v.
-  red O D (Vec O D ty v) M →
-  red O D (App O D (Vec O D ty v) (to_T O D ty a)) M1 →
-  assoc (FinSet_of_FType O D ty) (T O D) a (enum (FinSet_of_FType O D ty)) v
-    =Some (T O D) M2 →
-  ∃M3:T O D
-  .star (T O D) (red O D) M2 M3
-   ∧star (T O D) (red O D) (App O D M (to_T O D ty a)) M3.
-#O #D #ty #a #M #M1 #M2 #v #redM #redM1 #Ha lapply (red_vec … redM) -redM
-* #N * #N1 * #v1 * #v2 * * #Hred1 #Hv #HM0 >HM0 -HM0 >Hv in Ha; #Ha
-cases (same_assoc … a (enum (FinSet_of_FType O D ty)) v1 v2 N N1)
-  [* >Ha -Ha #H1 destruct (H1) #Ha
-   %{N1} (* CR-term *) % [@R_to_star //|@R_to_star @(riota … Ha)]
-  |#Ha1 %{M2} (* CR-term *) % [// | @R_to_star @riota <Ha1 @Ha]
-  ]
-qed.
-
-lemma nth_to_default: ∀A,l,n,d. 
-  |l| ≤ n → nth n A l d = d.
-#A #l elim l [//] #a #tl #Hind #n cases n
-  [#d normalize #H @False_ind @(absurd … H) @lt_to_not_le //
-  |#m #d normalize #H @Hind @le_S_S_to_le @H
-  ]
-qed.
-
-lemma nth_map: ∀A,B,l,f,n,d1,d2. 
-  n < |l| → nth n B (map … f l) d1 = f (nth n A l d2).
-#n #B #l #f elim l 
-  [#m #d1 #d2 normalize #H @False_ind @(absurd … H) @lt_to_not_le //
-  |#a #tl #Hind #m #d1 #d2 cases m normalize // 
-   #m1 #H @Hind @le_S_S_to_le @H
-  ]
-qed.
-
-lemma critical3: ∀O,D,ty,M1,M2. red O D M1 M2 → 
-  ∃M3:T O D.star (T O D) (red O D) (Lambda O D ty M2) M3
-   ∧star (T O D) (red O D)
-    (Vec O D ty
-     (map (FinSet_of_FType O D ty) (T O D)
-      (λa:FinSet_of_FType O D ty.subst O D M1 0 (to_T O D ty a))
-      (enum (FinSet_of_FType O D ty)))) M3.
-#O #D #ty #M1 #M2 #Hred
- %{(Vec O D ty
-    (map (FinSet_of_FType O D ty) (T O D)
-    (λa:FinSet_of_FType O D ty.subst O D M2 0 (to_T O D ty a))
-    (enum (FinSet_of_FType O D ty))))} (* CR-term *) %
-  [@R_to_star @rmem
-  |@star_red_vec2 [>length_map >length_map //] #n #M0
-   cases (true_or_false (leb (|enum (FinSet_of_FType O D ty)|) n)) #Hcase
-    [>nth_to_default [2:>length_map @(leb_true_to_le … Hcase)]
-     >nth_to_default [2:>length_map @(leb_true_to_le … Hcase)] //
-    |cut (n < |enum (FinSet_of_FType O D ty)|) 
-      [@not_le_to_lt @leb_false_to_not_le @Hcase] #Hlt
-     cut (∃a:FinSet_of_FType O D ty.True)
-      [lapply Hlt lapply (enum_complete (FinSet_of_FType O D ty))
-       cases (enum (FinSet_of_FType O D ty)) 
-        [#_ normalize #H @False_ind @(absurd … H) @lt_to_not_le //
-        |#a #l #_ #_ %{a} //
-        ]
-      ] * #a #_
-     >(nth_map ?????? a Hlt) >(nth_map ?????? a Hlt) 
-     @red_star_subst2 @R_to_star //
-    ]
-  ]
-qed.
-
-(* we need to proceed by structural induction on the term and then
-by inversion on the two redexes. The problem are the moves in a 
-same subterm, since we need an induction hypothesis, there *)
-
-lemma local_confluence: ∀O,D,M,M1,M2. red O D M M1 → red O D M M2 → 
-∃M3. star ? (red O D) M1 M3 ∧ star ? (red O D) M2 M3. 
-#O #D #M @(T_elim … M)
-  [#o #a #M1 #M2 #H elim(red_val ????? H)
-  |#n #M1 #M2 #H elim(red_rel ???? H)
-  |(* app : this is the interesting case *)
-   #P #Q #HindP #HindQ
-   #M1 #M2 #H1 inversion H1 -H1
-    [(* right redex is beta *)
-     #ty #Q #N #Hc #HM >HM -HM #HM1 >HM1 - HM1 #Hl inversion Hl
-      [#ty1 #Q1 #N1 #Hc1 #H1 destruct (H1) #H_ 
-       %{(subst O D Q1 0 N1)} (* CR-term *) /2/
-      |#ty #v #a #M0 #_ #H1 destruct (H1) (* vacuous *)
-      |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #_ cases (red_lambda … redM0)
-        [* #Q1 * #redQ #HM10 >HM10 
-         %{(subst O D Q1 0 N0)} (* CR-term *) %
-          [@red_star_subst2 @R_to_star //|@R_to_star @rbeta @Hc]
-        |#HM1 >HM1 @critical
-        ]
-      |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) #HM2
-       %{(subst O D Q 0 N1)} (* CR-term *) 
-       %[@red_star_subst @R_to_star //|@R_to_star @rbeta @(red_closed … Hc) //]
-      |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
-      |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
-      |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
-      ] 
-    |(* right redex is iota *)#ty #v #a #M3 #Ha #_ #_ #Hl inversion Hl
-      [#P1 #M1 #N1 #_ #H1 destruct (H1) (* vacuous *)
-      |#ty1 #v1 #a1 #M4 #Ha1 #H1 destruct (H1) -H1 #HM4 >(inj_to_T … e0) in Ha;
-       >Ha1 #H1 destruct (H1) %{M3} (* CR-term *) /2/
-      |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2 @(critical2 … redM0 Hl Ha)
-      |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) elim (normal_to_T … redN0N1)
-      |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
-      |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
-      |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
-      ]
-    |(* right redex is appl *)#M3 #M4 #N #redM3M4 #_ #H1 destruct (H1) #_ 
-      #Hl inversion Hl
-      [#ty1 #M1 #N1 #Hc #H1 destruct (H1) #HM2 lapply (red_lambda … redM3M4) *
-        [* #M3 * #H1 #H2 >H2 %{(subst O D M3 0 N1)} %
-          [@R_to_star @rbeta @Hc|@red_star_subst2 @R_to_star @H1]
-        |#H >H -H lapply (critical O D ty1 M1 N1) * #M3 * #H1 #H2 
-         %{M3} /2/
-        ]
-      |#ty1 #v1 #a1 #M4 #Ha1 #H1 #H2 destruct 
-       lapply (critical2 … redM3M4 Hl Ha1) * #M3 * #H1 #H2 %{M3} /2/
-      |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2 
-       lapply (HindP … redM0 redM3M4) * #M3 * #H1 #H2 
-       %{(App O D M3 N0)} (* CR-term *) % [@star_red_appl //|@star_red_appl //]
-      |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) #_
-       %{(App O D M4 N1)} % @R_to_star [@rappr //|@rappl //]
-      |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
-      |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
-      |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
-      ]
-    |(* right redex is appr *)#M3 #N #N1 #redN #_ #H1 destruct (H1) #_ 
-      #Hl inversion Hl
-      [#ty1 #M0 #N0 #Hc #H1 destruct (H1) #HM2 
-       %{(subst O D M0 0 N1)} (* CR-term *) % 
-        [@R_to_star @rbeta @(red_closed … Hc) //|@red_star_subst @R_to_star // ]
-      |#ty1 #v1 #a1 #M4 #Ha1 #H1 #H2 destruct (H1) elim (normal_to_T … redN)
-      |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2 
-       %{(App O D M10 N1)} (* CR-term *) % @R_to_star [@rappl //|@rappr //]
-      |#M0 #N0 #N10 #redN0 #_ #H1 destruct (H1) #_
-       lapply (HindQ … redN0 redN) * #M3 * #H1 #H2 
-       %{(App O D M0 M3)} (* CR-term *) % [@star_red_appr //|@star_red_appr //]
-      |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
-      |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
-      |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
-      ]
-    |(* right redex is rlam *) #ty #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
-    |(* right redex is rmem *) #ty #M0 #H1 destruct (H1) (* vacuous *)
-    |(* right redex is vec *) #ty #N #N1 #v #v1 #_ #_ 
-     #H1 destruct (H1) (* vacuous *)
-    ]
-  |#ty #M1 #Hind #M2 #M3 #H1 #H2 (* this case is not trivial any more *)
-   lapply (red_lambda … H1) *
-    [* #M4 * #H3 #H4 >H4 lapply (red_lambda … H2) *
-      [* #M5 * #H5 #H6 >H6 lapply(Hind … H3 H5) * #M6 * #H7 #H8 
-       %{(Lambda O D ty M6)} (* CR-term *) % @star_red_lambda //
-      |#H5 >H5 @critical3 // 
-      ]
-    |#HM2 >HM2 lapply (red_lambda … H2) *
-      [* #M4 * #Hred #HM3 >HM3 lapply (critical3 … ty ?? Hred) * #M5
-       * #H3 #H4 %{M5} (* CR-term *) % //
-      |#HM3 >HM3 %{M3} (* CR-term *) % // 
-      ]
-    ]
-  |#ty #v1 #Hind #M1 #M2 #H1 #H2
-   lapply (red_vec … H1) * #N11 * #N12 * #v11 * #v12 * * #redN11 #Hv1 #HM1
-   lapply (red_vec … H2) * #N21* #N22 * #v21 * #v22 * * #redN21 #Hv2 #HM2
-   >Hv1 in Hv2; #Hvv lapply (compare_append … Hvv) -Hvv * 
-   (* we must proceed by cases on the list *) * normalize
-    [(* N11 = N21 *) *
-      [>append_nil * #Hl1 #Hl2 destruct lapply(Hind N11 … redN11 redN21)
-        [@mem_append_l2 %1 //]
-       * #M3 * #HM31 #HM32
-       %{(Vec O D ty (v21@M3::v12))} (* CR-term *) 
-       % [@star_red_vec //|@star_red_vec //]
-      |>append_nil * #Hl1 #Hl2 destruct lapply(Hind N21 … redN21 redN11)
-        [@mem_append_l2 %1 //]
-       * #M3 * #HM31 #HM32
-       %{(Vec O D ty (v11@M3::v22))} (* CR-term *) 
-       % [@star_red_vec //|@star_red_vec //]
-      ]
-    |(* N11 ≠  N21 *) -Hind #P #l *
-      [* #Hv11 #Hv22 destruct
-       %{((Vec O D ty ((v21@N22::l)@N12::v12)))} (* CR-term *) % @R_to_star 
-        [>associative_append >associative_append normalize @rvec //
-        |>append_cons <associative_append <append_cons in ⊢ (???%?); @rvec //
-        ]
-      |* #Hv11 #Hv22 destruct
-       %{((Vec O D ty ((v11@N12::l)@N22::v22)))} (* CR-term *) % @R_to_star 
-        [>append_cons <associative_append <append_cons in ⊢ (???%?); @rvec //
-        |>associative_append >associative_append normalize @rvec //
-        ]
-      ]
-    ]
-  ]
-qed.    
-      
-
-
-
diff --git a/matita/matita/lib/finite_lambda/typing_deep.ma b/matita/matita/lib/finite_lambda/typing_deep.ma
deleted file mode 100644
index d2fde8760..000000000
--- a/matita/matita/lib/finite_lambda/typing_deep.ma
+++ /dev/null
@@ -1,239 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department of the University of Bologna, Italy.                     
-    ||I||                                                                 
-    ||T||  
-    ||A||  This file is distributed under the terms of the 
-    \   /  GNU General Public License Version 2        
-     \ /      
-      V_______________________________________________________________ *)
-
-include "finite_lambda/finite_lambda_deep.ma".
-
-
-(****************************************************************)
-
-inductive TJ (O: Type[0]) (D:O → FinSet): list (FType O) → T O D → FType O → Prop ≝
-  | tval: ∀G,o,a. TJ O D G (Val O D o a) (atom O o)
-  | trel: ∀G1,ty,G2,n. length ? G1 = n → TJ O D (G1@ty::G2) (Rel O D n) ty
-  | tapp: ∀G,M,N,ty1,ty2. TJ O D G M (arrow O ty1 ty2) → TJ O D G N ty1 →
-      TJ O D G (App O D M N) ty2
-  | tlambda: ∀G,M,ty1,ty2. TJ O D (ty1::G) M ty2 → 
-      TJ O D G (Lambda O D ty1 M) (arrow O ty1 ty2)
-  | tvec: ∀G,v,ty1,ty2.
-      (|v| = |enum (FinSet_of_FType O D ty1)|) →
-      (∀M. mem ? M v → TJ O D G M ty2) →
-      TJ O D G (Vec O D ty1 v) (arrow O ty1 ty2).
-
-lemma wt_to_T: ∀O,D,G,ty,a.TJ O D G (to_T O D ty a) ty.
-#O #D #G #ty elim ty
-  [#o #a normalize @tval
-  |#ty1 #ty2 #Hind1 #Hind2 normalize * #v #Hv @tvec
-    [<Hv >length_map >length_map //
-    |#M elim v 
-      [normalize @False_ind |#a #v1 #Hind3 * [#eqM >eqM @Hind2 |@Hind3]]
-    ]
-  ]
-qed.
-
-lemma inv_rel: ∀O,D,G,n,ty.
-  TJ O D G (Rel O D n) ty → ∃G1,G2.|G1|=n∧G=G1@ty::G2.
-#O #D #G #n #ty #Hrel inversion Hrel
-  [#G1 #o #a #_ #H destruct 
-  |#G1 #ty1 #G2 #n1 #H1 #H2 #H3 #H4 destruct %{G1} %{G2} /2/ 
-  |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct
-  |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct 
-  |#G1 #v #ty3 #ty4 #_ #_ #_ #_ #H destruct 
-  ]
-qed.
-      
-lemma inv_tlambda: ∀O,D,G,M,ty1,ty2,ty3.
-  TJ O D G (Lambda O D ty1 M) (arrow O ty2 ty3) → 
-  ty1 = ty2 ∧ TJ O D (ty2::G) M ty3.
-#O #D #G #M #ty1 #ty2 #ty3 #Hlam inversion Hlam
-  [#G1 #o #a #_ #H destruct 
-  |#G1 #ty #G2 #n #_ #_ #H destruct
-  |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct
-  |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct % //
-  |#G1 #v #ty3 #ty4 #_ #_ #_ #_ #H destruct 
-  ]
-qed.
-
-lemma inv_tvec: ∀O,D,G,v,ty1,ty2,ty3.
-   TJ O D G (Vec O D ty1 v) (arrow O ty2 ty3) →
-  (|v| = |enum (FinSet_of_FType O D ty1)|) ∧
-  (∀M. mem ? M v → TJ O D G M ty3).
-#O #D #G #v #ty1 #ty2 #ty3 #Hvec inversion Hvec
-  [#G #o #a #_ #H destruct 
-  |#G1 #ty #G2 #n #_ #_ #H destruct
-  |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct
-  |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct 
-  |#G1 #v1 #ty4 #ty5 #Hv #Hmem #_ #_ #H #H1 destruct % // @Hmem 
-  ]
-qed.
-
-(* could be generalized *)
-lemma weak_rel: ∀O,D,G1,G2,ty1,ty2,n. length ? G1 < n → 
-   TJ O D (G1@G2) (Rel O D n) ty1 →
-   TJ O D (G1@ty2::G2) (Rel O D (S n)) ty1.
-#O #D #G1 #G2 #ty1 #ty2 #n #HG1 #Hrel lapply (inv_rel … Hrel)
-* #G3 * #G4 * #H1 #H2 lapply (compare_append … H2)
-* #G5 *
-  [* #H3 @False_ind >H3 in HG1; >length_append >H1 #H4
-   @(absurd … H4) @le_to_not_lt //
-  |* #H3 #H4 >H4 >append_cons <associative_append @trel
-   >length_append >length_append <H1 >H3 >length_append normalize 
-   >plus_n_Sm >associative_plus @eq_f //
-  ]
-qed.
-
-lemma strength_rel: ∀O,D,G1,G2,ty1,ty2,n. length ? G1 < n → 
-   TJ O D (G1@ty2::G2) (Rel O D n) ty1 →
-   TJ O D (G1@G2) (Rel O D (n-1)) ty1.
-#O #D #G1 #G2 #ty1 #ty2 #n #HG1 #Hrel lapply (inv_rel … Hrel)
-* #G3 * #G4 * #H1 #H2 lapply (compare_append … H2)
-* #G5 *
-  [* #H3 @False_ind >H3 in HG1; >length_append >H1 #H4
-   @(absurd … H4) @le_to_not_lt //
-  |lapply G5 -G5 * 
-    [>append_nil normalize * #H3 #H4 destruct @False_ind @(absurd … HG1) 
-     @le_to_not_lt //
-    |#ty3 #G5 * #H3 normalize #H4 destruct (H4) <associative_append @trel
-     <H1 >H3 >length_append >length_append normalize <plus_minus_associative //
-    ]
-  ]
-qed.
-
-lemma weakening: ∀O,D,G,N,tyN. 
-  TJ O D G N tyN →  ∀G1,G2,G3.G=G1@G2 → 
-    TJ O D (G1@G3@G2) (lift O D N (|G1|) (|G3|)) tyN.    
-#O #D #G #N #tyN #HN elim HN -HN -tyN -N -G 
-  [#G #o #a #G1 #G2 #G3 #_ @tval 
-  |#G #ty #G2 #n #HG #G3 #G4 #G5 #H normalize 
-   cases (true_or_false (leb (|G3|) n)) #Hcase >Hcase normalize
-    [lapply (compare_append … H) * #G6 *
-      [* #H1 #H2 >H2 <associative_append <associative_append @trel
-       <HG >H1 >length_append >length_append >length_append //
-      |cases G6 
-        [* >append_nil normalize #H1 #H2 <H2 <associative_append @trel
-         <HG >H1 >length_append //
-        |#ty1 #G7 * #H @False_ind @(absurd … (leb_true_to_le … Hcase))
-         @lt_to_not_le <HG >H >length_append normalize //
-        ]
-      ]
-    |lapply (compare_append … H) * #G6 *
-      [* #H1 @False_ind @(absurd ?? (leb_false_to_not_le … Hcase)) <HG >H1
-       >length_append normalize //
-      |* cases G6
-        [>append_nil normalize #H1 @False_ind 
-         @(absurd ?? (leb_false_to_not_le … Hcase)) <HG >H1 //
-        |#ty1 #G7 #H1 normalize #H2 destruct >associative_append @trel //
-        ]
-      ]
-    ]
-  |#G #M #N #ty1 #ty2 #HM #HN #HindM #HindN #G1 #G2 #G3 
-   #Heq @(tapp … (HindM … Heq) (HindN … Heq))
-  |#G #M #ty1 #ty2 #HM #HindM #G1 #G2 #G3 #Heq @tlambda @(HindM (ty1::G1)) 
-   >Heq //
-  |#G #v #ty1 #ty2 #Hlen #Hv #Hind #G1 #G2 #G3 #H1 @tvec 
-    [>length_map // 
-    |#M #Hmem lapply (mem_map ????? Hmem) * #M1 * #memM1 #eqM <eqM @Hind //
-    ]
-  ]
-qed.
-
-lemma nth_spec: ∀A,a,d,l1,l2,n. |l1| = n → nth n A (l1@a::l2) d = a.
-#A #a #d #l1 elim l1 normalize
-  [#l2 #n #Hn <Hn  //
-  |#b #tl #Hind #l2 #m #Hm <Hm normalize @Hind //
-  ]
-qed.
-             
-lemma wt_subst_gen: ∀O,D,G,M,tyM. 
-  TJ O D G M tyM → 
-   ∀G1,G2,N,tyN.G=(G1@tyN::G2) →
-    TJ O D G2 N tyN →
-     TJ O D (G1@G2) (subst O D M (|G1|) N) tyM.
-#O #D #G #M #tyM #HM elim HM -HM -tyM -M -G
-  [#G #o #a #G1 #G2 #N #tyN #HG #_ normalize @tval
-  |#G #ty #G2 #n #Hlen #G21 #G22 #N #tyN #HG #HN 
-   normalize cases (true_or_false (leb (|G21|) n))
-    [#H >H cases (le_to_or_lt_eq … (leb_true_to_le … H))
-      [#ltn >(not_eq_to_eqb_false … (lt_to_not_eq … ltn)) normalize
-       lapply (compare_append … HG) * #G3 *
-        [* #HG1 #HG2 @(strength_rel … tyN … ltn) <HG @trel @Hlen
-        |* #HG >HG in ltn; >length_append #ltn @False_ind 
-         @(absurd … ltn) @le_to_not_lt >Hlen //
-        ] 
-      |#HG21 >(eq_to_eqb_true … HG21) 
-       cut (ty = tyN) 
-        [<(nth_spec ? ty ty ? G2 … Hlen) >HG @nth_spec @HG21] #Hty >Hty
-       normalize <HG21 @(weakening ????? HN [ ]) //
-      ]
-    |#H >H normalize lapply (compare_append … HG) * #G3 *
-      [* #H1 @False_ind @(absurd ? Hlen) @sym_not_eq @lt_to_not_eq >H1
-       >length_append @(lt_to_le_to_lt n (|G21|)) // @not_le_to_lt
-       @(leb_false_to_not_le … H) 
-      |cases G3 
-        [>append_nil * #H1 @False_ind @(absurd ? Hlen) <H1 @sym_not_eq
-         @lt_to_not_eq @not_le_to_lt @(leb_false_to_not_le … H)
-        |#ty2 #G4 * #H1 normalize #H2 destruct >associative_append @trel //
-        ]
-      ]    
-    ]
-  |#G #M #N #ty1 #ty2 #HM #HN #HindM #HindN #G1 #G2 #N0 #tyN0 #eqG
-   #HN0 normalize @(tapp … ty1) [@(HindM … eqG HN0) |@(HindN … eqG HN0)]
-  |#G #M #ty1 #ty2 #HM #HindM #G1 #G2 #N0 #tyN0 #eqG
-   #HN0 normalize @(tlambda … ty1) @(HindM (ty1::G1) … HN0) >eqG //
-  |#G #v #ty1 #ty2 #Hlen #Hv #Hind #G1 #G2 #N0 #tyN0 #eqG
-   #HN0 normalize @(tvec … ty1) 
-    [>length_map @Hlen
-    |#M #Hmem lapply (mem_map ????? Hmem) * #a * -Hmem #Hmem #eqM <eqM
-     @(Hind … Hmem … eqG HN0) 
-    ]
-  ]
-qed.
-
-lemma wt_subst: ∀O,D,M,N,G,ty1,ty2. 
-  TJ O D (ty1::G) M ty2 → 
-  TJ O D G N ty1 →
-  TJ O D G (subst O D M 0 N) ty2.
-#O #D #M #N #G #ty1 #ty2 #HM #HN @(wt_subst_gen …(ty1::G) … [ ] … HN) //
-qed.
-
-lemma subject_reduction: ∀O,D,M,M1,G,ty. 
-  TJ O D G M ty → red O D M M1 → TJ O D G M1 ty.
-#O #D #M #M1 #G #ty #HM lapply M1 -M1 elim HM  -HM -ty -G -M
-  [#G #o #a #M1 #Hval elim (red_val ????? Hval)
-  |#G #ty #G1 #n #_ #M1 #Hrel elim (red_rel ???? Hrel) 
-  |#G #M #N #ty1 #ty2 #HM #HN #HindM #HindN #M1 #Hred inversion Hred
-    [#P #M0 #N0 #Hc #H1 destruct (H1) #HM1 @(wt_subst … HN)
-     @(proj2 … (inv_tlambda … HM))
-    |#ty #v #a #M0 #Ha #H1 #H2 destruct @(proj2 … (inv_tvec … HM))
-     @(assoc_to_mem … Ha)
-    |#M2 #M3 #N0 #Hredl #_ #H1 destruct (H1) #eqM1 @(tapp … HN) @HindM @Hredl
-    |#M2 #M3 #N0 #Hredr #_ #H1 destruct (H1) #eqM1 @(tapp … HM) @HindN @Hredr
-    |#ty #N0 #N1 #_ #_ #H1 destruct (H1)
-    |#ty #M0 #H1 destruct (H1)
-    |#ty #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1)
-    ]
-  |#G #P #ty1 #ty2 #HP #Hind #M1 #Hred lapply(red_lambda ????? Hred) *
-    [* #P1 * #HredP #HM1 >HM1 @tlambda @Hind //
-    |#HM1 >HM1 @tvec // #N #HN lapply(mem_map ????? HN) 
-     * #a * #mema #eqN <eqN -eqN @(wt_subst …HP) @wt_to_T
-    ]
-  |#G #v #ty1 #ty2 #Hlen #Hv #Hind #M1 #Hred lapply(red_vec ????? Hred)
-   * #N * #N1 * #v1 * #v2 * * #H1 #H2 #H3 >H3 @tvec 
-    [<Hlen >H2 >length_append >length_append @eq_f //
-    |#M2 #Hmem cases (mem_append ???? Hmem) -Hmem #Hmem
-      [@Hv >H2 @mem_append_l1 //
-      |cases Hmem 
-        [#HM2 >HM2 -HM2 @(Hind N … H1) >H2 @mem_append_l2 %1 //
-        |-Hmem #Hmem @Hv >H2 @mem_append_l2 %2 //
-        ]
-      ]
-    ]
-  ]
-qed.
-    
diff --git a/matita/matita/lib/finite_lambda/typing_old.ma b/matita/matita/lib/finite_lambda/typing_old.ma
deleted file mode 100644
index 7ab0bdbfd..000000000
--- a/matita/matita/lib/finite_lambda/typing_old.ma
+++ /dev/null
@@ -1,236 +0,0 @@
-(*
-    ||M||  This file is part of HELM, an Hypertextual, Electronic        
-    ||A||  Library of Mathematics, developed at the Computer Science     
-    ||T||  Department of the University of Bologna, Italy.                     
-    ||I||                                                                 
-    ||T||  
-    ||A||  This file is distributed under the terms of the 
-    \   /  GNU General Public License Version 2        
-     \ /      
-      V_______________________________________________________________ *)
-
-include "finite_lambda/finite_lambda.ma".
-
-
-(****************************************************************)
-
-inductive TJ (O: Type[0]) (D:O → FinSet): list (FType O) → T O D → FType O → Prop ≝
-  | tval: ∀G,o,a. TJ O D G (Val O D o a) (atom O o)
-  | trel: ∀G1,ty,G2,n. length ? G1 = n → TJ O D (G1@ty::G2) (Rel O D n) ty
-  | tapp: ∀G,M,N,ty1,ty2. TJ O D G M (arrow O ty1 ty2) → TJ O D G N ty1 →
-      TJ O D G (App O D M N) ty2
-  | tlambda: ∀G,M,ty1,ty2. TJ O D (ty1::G) M ty2 → 
-      TJ O D G (Lambda O D ty1 M) (arrow O ty1 ty2)
-  | tvec: ∀G,v,ty1,ty2.
-      (|v| = |enum (FinSet_of_FType O D ty1)|) →
-      (∀M. mem ? M v → TJ O D G M ty2) →
-      TJ O D G (Vec O D ty1 v) (arrow O ty1 ty2).
-
-lemma wt_to_T: ∀O,D,G,ty,a.TJ O D G (to_T O D ty a) ty.
-#O #D #G #ty elim ty
-  [#o #a normalize @tval
-  |#ty1 #ty2 #Hind1 #Hind2 normalize * #v #Hv @tvec
-    [<Hv >length_map >length_map //
-    |#M elim v 
-      [normalize @False_ind |#a #v1 #Hind3 * [#eqM >eqM @Hind2 |@Hind3]]
-    ]
-  ]
-qed.
-
-lemma inv_rel: ∀O,D,G,n,ty.
-  TJ O D G (Rel O D n) ty → ∃G1,G2.|G1|=n∧G=G1@ty::G2.
-#O #D #G #n #ty #Hrel inversion Hrel
-  [#G1 #o #a #_ #H destruct 
-  |#G1 #ty1 #G2 #n1 #H1 #H2 #H3 #H4 destruct %{G1} %{G2} /2/ 
-  |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct
-  |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct 
-  |#G1 #v #ty3 #ty4 #_ #_ #_ #_ #H destruct 
-  ]
-qed.
-      
-lemma inv_tlambda: ∀O,D,G,M,ty1,ty2,ty3.
-  TJ O D G (Lambda O D ty1 M) (arrow O ty2 ty3) → 
-  ty1 = ty2 ∧ TJ O D (ty2::G) M ty3.
-#O #D #G #M #ty1 #ty2 #ty3 #Hlam inversion Hlam
-  [#G1 #o #a #_ #H destruct 
-  |#G1 #ty #G2 #n #_ #_ #H destruct
-  |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct
-  |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct % //
-  |#G1 #v #ty3 #ty4 #_ #_ #_ #_ #H destruct 
-  ]
-qed.
-
-lemma inv_tvec: ∀O,D,G,v,ty1,ty2,ty3.
-   TJ O D G (Vec O D ty1 v) (arrow O ty2 ty3) →
-  (|v| = |enum (FinSet_of_FType O D ty1)|) ∧
-  (∀M. mem ? M v → TJ O D G M ty3).
-#O #D #G #v #ty1 #ty2 #ty3 #Hvec inversion Hvec
-  [#G #o #a #_ #H destruct 
-  |#G1 #ty #G2 #n #_ #_ #H destruct
-  |#G1 #M0 #N #ty1 #ty2 #_ #_ #_ #_ #_ #H destruct
-  |#G1 #M0 #ty4 #ty5 #HM0 #_ #_ #H #H1 destruct 
-  |#G1 #v1 #ty4 #ty5 #Hv #Hmem #_ #_ #H #H1 destruct % // @Hmem 
-  ]
-qed.
-
-(* could be generalized *)
-lemma weak_rel: ∀O,D,G1,G2,ty1,ty2,n. length ? G1 < n → 
-   TJ O D (G1@G2) (Rel O D n) ty1 →
-   TJ O D (G1@ty2::G2) (Rel O D (S n)) ty1.
-#O #D #G1 #G2 #ty1 #ty2 #n #HG1 #Hrel lapply (inv_rel … Hrel)
-* #G3 * #G4 * #H1 #H2 lapply (compare_append … H2)
-* #G5 *
-  [* #H3 @False_ind >H3 in HG1; >length_append >H1 #H4
-   @(absurd … H4) @le_to_not_lt //
-  |* #H3 #H4 >H4 >append_cons <associative_append @trel
-   >length_append >length_append <H1 >H3 >length_append normalize 
-   >plus_n_Sm >associative_plus @eq_f //
-  ]
-qed.
-
-lemma strength_rel: ∀O,D,G1,G2,ty1,ty2,n. length ? G1 < n → 
-   TJ O D (G1@ty2::G2) (Rel O D n) ty1 →
-   TJ O D (G1@G2) (Rel O D (n-1)) ty1.
-#O #D #G1 #G2 #ty1 #ty2 #n #HG1 #Hrel lapply (inv_rel … Hrel)
-* #G3 * #G4 * #H1 #H2 lapply (compare_append … H2)
-* #G5 *
-  [* #H3 @False_ind >H3 in HG1; >length_append >H1 #H4
-   @(absurd … H4) @le_to_not_lt //
-  |lapply G5 -G5 * 
-    [>append_nil normalize * #H3 #H4 destruct @False_ind @(absurd … HG1) 
-     @le_to_not_lt //
-    |#ty3 #G5 * #H3 normalize #H4 destruct (H4) <associative_append @trel
-     <H1 >H3 >length_append >length_append normalize <plus_minus_associative //
-    ]
-  ]
-qed.
-
-lemma weakening: ∀O,D,G,N,tyN. 
-  TJ O D G N tyN →  ∀G1,G2,G3.G=G1@G2 → 
-    TJ O D (G1@G3@G2) (lift O D N (|G1|) (|G3|)) tyN.    
-#O #D #G #N #tyN #HN elim HN -HN -tyN -N -G 
-  [#G #o #a #G1 #G2 #G3 #_ @tval 
-  |#G #ty #G2 #n #HG #G3 #G4 #G5 #H normalize 
-   cases (true_or_false (leb (|G3|) n)) #Hcase >Hcase normalize
-    [lapply (compare_append … H) * #G6 *
-      [* #H1 #H2 >H2 <associative_append <associative_append @trel
-       <HG >H1 >length_append >length_append >length_append //
-      |cases G6 
-        [* >append_nil normalize #H1 #H2 <H2 <associative_append @trel
-         <HG >H1 >length_append //
-        |#ty1 #G7 * #H @False_ind @(absurd … (leb_true_to_le … Hcase))
-         @lt_to_not_le <HG >H >length_append normalize //
-        ]
-      ]
-    |lapply (compare_append … H) * #G6 *
-      [* #H1 @False_ind @(absurd ?? (leb_false_to_not_le … Hcase)) <HG >H1
-       >length_append normalize //
-      |* cases G6
-        [>append_nil normalize #H1 @False_ind 
-         @(absurd ?? (leb_false_to_not_le … Hcase)) <HG >H1 //
-        |#ty1 #G7 #H1 normalize #H2 destruct >associative_append @trel //
-        ]
-      ]
-    ]
-  |#G #M #N #ty1 #ty2 #HM #HN #HindM #HindN #G1 #G2 #G3 
-   #Heq @(tapp … (HindM … Heq) (HindN … Heq))
-  |#G #M #ty1 #ty2 #HM #HindM #G1 #G2 #G3 #Heq @tlambda @(HindM (ty1::G1)) 
-   >Heq //
-  |#G #v #ty1 #ty2 #Hlen #Hv #Hind #G1 #G2 #G3 #H1 @tvec 
-    [>length_map // 
-    |#M #Hmem lapply (mem_map ????? Hmem) * #M1 * #memM1 #eqM <eqM @Hind //
-    ]
-  ]
-qed.
-
-lemma nth_spec: ∀A,a,d,l1,l2,n. |l1| = n → nth n A (l1@a::l2) d = a.
-#A #a #d #l1 elim l1 normalize
-  [#l2 #n #Hn <Hn  //
-  |#b #tl #Hind #l2 #m #Hm <Hm normalize @Hind //
-  ]
-qed.
-             
-lemma wt_subst_gen: ∀O,D,G,M,tyM. 
-  TJ O D G M tyM → 
-   ∀G1,G2,N,tyN.G=(G1@tyN::G2) →
-    TJ O D G2 N tyN →
-     TJ O D (G1@G2) (subst O D M (|G1|) N) tyM.
-#O #D #G #M #tyM #HM elim HM -HM -tyM -M -G
-  [#G #o #a #G1 #G2 #N #tyN #HG #_ normalize @tval
-  |#G #ty #G2 #n #Hlen #G21 #G22 #N #tyN #HG #HN 
-   normalize cases (true_or_false (leb (|G21|) n))
-    [#H >H cases (le_to_or_lt_eq … (leb_true_to_le … H))
-      [#ltn >(not_eq_to_eqb_false … (lt_to_not_eq … ltn)) normalize
-       lapply (compare_append … HG) * #G3 *
-        [* #HG1 #HG2 @(strength_rel … tyN … ltn) <HG @trel @Hlen
-        |* #HG >HG in ltn; >length_append #ltn @False_ind 
-         @(absurd … ltn) @le_to_not_lt >Hlen //
-        ] 
-      |#HG21 >(eq_to_eqb_true … HG21) 
-       cut (ty = tyN) 
-        [<(nth_spec ? ty ty ? G2 … Hlen) >HG @nth_spec @HG21] #Hty >Hty
-       normalize <HG21 @(weakening ????? HN [ ]) //
-      ]
-    |#H >H normalize lapply (compare_append … HG) * #G3 *
-      [* #H1 @False_ind @(absurd ? Hlen) @sym_not_eq @lt_to_not_eq >H1
-       >length_append @(lt_to_le_to_lt n (|G21|)) // @not_le_to_lt
-       @(leb_false_to_not_le … H) 
-      |cases G3 
-        [>append_nil * #H1 @False_ind @(absurd ? Hlen) <H1 @sym_not_eq
-         @lt_to_not_eq @not_le_to_lt @(leb_false_to_not_le … H)
-        |#ty2 #G4 * #H1 normalize #H2 destruct >associative_append @trel //
-        ]
-      ]    
-    ]
-  |#G #M #N #ty1 #ty2 #HM #HN #HindM #HindN #G1 #G2 #N0 #tyN0 #eqG
-   #HN0 normalize @(tapp … ty1) [@(HindM … eqG HN0) |@(HindN … eqG HN0)]
-  |#G #M #ty1 #ty2 #HM #HindM #G1 #G2 #N0 #tyN0 #eqG
-   #HN0 normalize @(tlambda … ty1) @(HindM (ty1::G1) … HN0) >eqG //
-  |#G #v #ty1 #ty2 #Hlen #Hv #Hind #G1 #G2 #N0 #tyN0 #eqG
-   #HN0 normalize @(tvec … ty1) 
-    [>length_map @Hlen
-    |#M #Hmem lapply (mem_map ????? Hmem) * #a * -Hmem #Hmem #eqM <eqM
-     @(Hind … Hmem … eqG HN0) 
-    ]
-  ]
-qed.
-
-lemma wt_subst: ∀O,D,M,N,G,ty1,ty2. 
-  TJ O D (ty1::G) M ty2 → 
-  TJ O D G N ty1 →
-  TJ O D G (subst O D M 0 N) ty2.
-#O #D #M #N #G #ty1 #ty2 #HM #HN @(wt_subst_gen …(ty1::G) … [ ] … HN) //
-qed.
-
-lemma subject_reduction: ∀O,D,M,M1,G,ty. 
-  TJ O D G M ty → red O D M M1 → TJ O D G M1 ty.
-#O #D #M #M1 #G #ty #HM lapply M1 -M1 elim HM  -HM -ty -G -M
-  [#G #o #a #M1 #Hval elim (red_val ????? Hval)
-  |#G #ty #G1 #n #_ #M1 #Hrel elim (red_rel ???? Hrel) 
-  |#G #M #N #ty1 #ty2 #HM #HN #HindM #HindN #M1 #Hred inversion Hred
-    [#P #M0 #N0 #H1 destruct (H1) #HM1 @(wt_subst … HN)
-     @(proj2 … (inv_tlambda … HM))
-    |#ty #v #a #M0 #Ha #H1 #H2 destruct @(proj2 … (inv_tvec … HM))
-     @(assoc_to_mem … Ha)
-    |#M2 #M3 #N0 #Hredl #_ #H1 destruct (H1) #eqM1 @(tapp … HN) @HindM @Hredl
-    |#M2 #M3 #N0 #Hredr #_ #H1 destruct (H1) #eqM1 @(tapp … HM) @HindN @Hredr
-    |#ty #M0 #H1 destruct (H1)
-    |#ty #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1)
-    ]
-  |#G #P #ty1 #ty2 #HP #Hind #M1 #Hred lapply(red_lambda ????? Hred) #HM1 >HM1
-   @tvec // #N #HN lapply(mem_map ????? HN) * #a * #mema #eqN <eqN -eqN
-   @(wt_subst …HP) @wt_to_T
-  |#G #v #ty1 #ty2 #Hlen #Hv #Hind #M1 #Hred lapply(red_vec ????? Hred)
-   * #N * #N1 * #v1 * #v2 * * #H1 #H2 #H3 >H3 @tvec 
-    [<Hlen >H2 >length_append >length_append @eq_f //
-    |#M2 #Hmem cases (mem_append ???? Hmem) -Hmem #Hmem
-      [@Hv >H2 @mem_append_l1 //
-      |cases Hmem 
-        [#HM2 >HM2 -HM2 @(Hind N … H1) >H2 @mem_append_l2 %1 //
-        |-Hmem #Hmem @Hv >H2 @mem_append_l2 %2 //
-        ]
-      ]
-    ]
-  ]
-qed.
-    
-- 
2.39.2