X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2FPTS%2Fgpts.ma;h=9af90225239158d425d63dd8cd90d8b2fbc2b1a7;hb=b1736386d7728463cfcc7b3539633db9154809b5;hp=bf149812dff02552e64dca5120802446df2158d4;hpb=ed76333464d49a3cd55ca2adb05b0afdbc8486bd;p=helm.git

diff --git a/helm/software/matita/nlibrary/PTS/gpts.ma b/helm/software/matita/nlibrary/PTS/gpts.ma
index bf149812d..9af902252 100644
--- a/helm/software/matita/nlibrary/PTS/gpts.ma
+++ b/helm/software/matita/nlibrary/PTS/gpts.ma
@@ -12,393 +12,65 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basics/list2.ma".
-
-ninductive T : Type ≝
-  | Sort: nat → T
-  | Rel: nat → T 
-  | App: T → T → T 
-  | Lambda: T → T → T (* type, body *)
-  | Prod: T → T → T (* type, body *)
-.
-
-nlet rec lift_aux t k p ≝
-  match t with 
-    [ Sort n ⇒ Sort n
-    | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n) (Rel (n+p))
-    | App m n ⇒ App (lift_aux m k p) (lift_aux n k p)
-    | Lambda m n ⇒ Lambda (lift_aux m k p) (lift_aux n (k+1) p)
-    | Prod m n ⇒ Prod (lift_aux m k p) (lift_aux n (k+1) p)
-    ].
+include "PTS/subst.ma".
 
-ndefinition lift ≝ λt.λp.lift_aux t 0 p.
+(*************************** substl *****************************)
 
-nlet rec subst_aux t k a ≝ 
-  match t with 
-    [ Sort n ⇒ Sort n
-    | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n)
-        (if_then_else T (eqb n k) (lift a n) (Rel (n-1)))
-    | App m n ⇒ App (subst_aux m k a) (subst_aux n k a)
-    | Lambda m n ⇒ Lambda (subst_aux m k a) (subst_aux n (k+1) a)
-    | Prod m n ⇒ Prod (subst_aux m k a) (subst_aux n (k+1) a)
+nlet rec substl (G:list T) (N:T) : list T ≝  
+  match G with
+    [ nil ⇒ nil T
+    | cons A D ⇒ ((subst A (length T D) N)::(substl D N))
     ].
 
-ndefinition subst ≝ λa.λt.subst_aux t 0 a.
-
-(*** properties of lift and subst ***)
-nlemma lift_aux_0: ∀t:T.∀k. lift_aux t k 0 = t.
-#t; nelim t; nnormalize; //; #n; #k; ncases (leb (S n) k); 
-nnormalize;//;nqed.
-
-nlemma lift_0: ∀t:T. lift t 0 = t.
-#t; nelim t; nnormalize; //; nqed.
-
-nlemma lift_sort: ∀i,k. lift (Sort i) k = Sort i.
-//; nqed.
-
-nlemma lift_rel: ∀i,k. lift (Rel i) k = Rel (i+k).
-//; nqed.
-
-nlemma lift_rel1: ∀i.lift (Rel i) 1 = Rel (S i).
-#i; nchange with (lift (Rel i) 1 = Rel (1 + i)); //; nqed.
-
 (*
-nlemma lift_lift_aux: ∀t.∀i,j,k,k1. k ≤ k1 → k1 ≤ k+j → 
-lift_aux (lift_aux t k j) k1 i = lift_aux t k (j+i).
-#t; nelim t; nnormalize; //; #n; #i;#j; #k; #k1; #lel; #ler; 
-napply (leb_elim (S n) k); #Hnk;nnormalize;
-  ##[nrewrite > (le_to_leb_true ? ? Hnk);nnormalize;//;
-  ##|nrewrite > (lt_to_leb_false (S n+j) k ?); 
-     nnormalize;//;napply (lt_to_le_to_lt ? (S n));
-      ##[napply not_le_to_lt;/2/;
-      ##|(* lento /2/; *) napply le_S_S;/1/;
-  ##]
-nqed. *)
-
-nlemma lift_lift_aux: ∀t.∀i,j,k. lift_aux (lift_aux t k j) k i = lift_aux t k (j+i).
-#t; nelim t; nnormalize; //; #n; #i;#j; #k; 
-napply (leb_elim (S n) k); #Hnk;nnormalize;
-  ##[nrewrite > (le_to_leb_true ? ? Hnk);nnormalize;//;
-  ##|nrewrite > (lt_to_leb_false (S n+j) k ?); 
-     nnormalize;//; napply (lt_to_le_to_lt ? (S n));
-      ##[napply not_le_to_lt;//;
-      ##|napply le_S_S;//;
-  ##]
-nqed.
-
-nlemma lift_lift_aux1: ∀t.∀i,j,k. lift_aux (lift_aux t k j) (j+k) i = lift_aux t k (j+i).
-#t; nelim t; nnormalize; //; #n; #i;#j; #k; 
-napply (leb_elim (S n) k); #Hnk;nnormalize;
-  ##[nrewrite > (le_to_leb_true (S n) (j+k) ?);nnormalize;/2/;
-  ##|nrewrite > (lt_to_leb_false (S n+j) (j+k) ?); 
-     nnormalize;//; napply le_S_S; napplyS monotonic_le_plus_r;
-     /3/;
-  ##]
-nqed.
-
-nlemma lift_lift_aux2: ∀t.∀i,j.j ≤ i  → ∀h,k. 
-lift_aux (lift_aux t k i) (j+k) h = lift_aux t k (i+h).
-#t; #i; #j; #h; nelim t; nnormalize; //; #n; #h;#k;
-napply (leb_elim (S n) k); #Hnk;nnormalize;
-  ##[nrewrite > (le_to_leb_true (S n) (j+k) ?);nnormalize;/2/;
-  ##|nrewrite > (lt_to_leb_false (S n+i) (j+k) ?); 
-     nnormalize;//;napply le_S_S; nrewrite > (symmetric_plus j k);
-     napply le_plus;//;napply not_lt_to_le;/2/;
-  ##]
-nqed.
-
-nlemma lift_lift: ∀t.∀i,j. lift (lift t j) i = lift t (j+i).
-nnormalize; //;
-nqed.
-
-nlemma subst_lift_aux_k: ∀A,B.∀k. 
-  subst_aux (lift_aux B k 1) k A = B.
-#A; #B; nelim B; nnormalize; /2/; #n; #k;
-napply (leb_elim (S n) k); nnormalize; #Hnk;
-  ##[nrewrite > (le_to_leb_true ?? Hnk);nnormalize;//;
-  ##|nrewrite > (lt_to_leb_false (S (n + 1)) k ?); nnormalize;
-      ##[nrewrite > (not_eq_to_eqb_false (n+1) k ?);
-         nnormalize;/2/; napply (not_to_not … Hnk);//;
-      ##|napply le_S; napplyS (not_le_to_lt (S n) k Hnk);
-      ##]
-  ##]
-nqed.
-
-nlemma subst_lift: ∀A,B. subst A (lift B 1) = B.
-nnormalize; //; nqed.
-
-nlemma subst_aux_sort: ∀A.∀n,k. subst_aux (Sort n) k A = Sort n.
+nlemma substl_cons: ∀A,N.∀G.
+substl (A::G) N = (subst_aux A (length T G) N)::(substl G N).
 //; nqed.
-
-nlemma subst_sort: ∀A.∀n. subst A (Sort n) = Sort n.
-//; nqed.
-
-nlemma subst_rel: ∀A.subst A (Rel O) = A.
-nnormalize; //; nqed.
-
-nlemma subst_rel1: ∀A.∀k,i. i < k → 
-  subst_aux (Rel i) k A = Rel i.
-#A; #k; #i; nnormalize; #ltik;
-nrewrite > (le_to_leb_true (S i) k ?); //; nqed.
-
-nlemma subst_rel2: ∀A.∀k. subst_aux (Rel k) k A = lift A k.
-#A; #k; nnormalize; 
-nrewrite > (lt_to_leb_false (S k) k ?); //; 
-nrewrite > (eq_to_eqb_true … (refl …)); //;
-nqed.
-
-nlemma subst_rel3: ∀A.∀k,i. k < i → 
-  subst_aux (Rel i) k A = Rel (i-1).
-#A; #k; #i; nnormalize; #ltik;
-nrewrite > (lt_to_leb_false (S i) k ?); /2/; 
-nrewrite > (not_eq_to_eqb_false i k ?); //;
-napply nmk; #eqik; nelim (lt_to_not_eq … (ltik …)); /2/;
-nqed.
-
-(* versione con plus 
-nlemma lift_subst_aux_k: ∀A,B.∀j,k.
-  lift_aux (subst_aux B (j+k) A) k 1 = subst_aux (lift_aux B k 1) (j+k+1) A.
-#A; #B; #j; nelim B; nnormalize; /2/; #n; #k;
-napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk;
-  ##[nelim (leb (S n) k); 
-    ##[nrewrite > (subst_rel1 A (j+k+1) n ?);/2/;
-    ##|nrewrite > (subst_rel1 A (j+k+1) (n+1) ?);/2/;
-    ##]
-  ##|napply (eqb_elim n (j+k)); nnormalize; #Heqnjk; 
-    ##[nrewrite > (lt_to_leb_false (S n) k ?);
-       ##[ncut (j+k+1 = n+1);##[//;##] #Heq;
-          nrewrite > Heq; nrewrite > (subst_rel2 A ?); nnormalize;
-          napplyS lift_lift_aux2 (* bello *);//;
-       ##|/2/;
-       ##]
-    ##|ncut (j + k < n);
-      ##[napply not_eq_to_le_to_lt;
-        ##[/2/;##|napply le_S_S_to_le;napply not_le_to_lt;/2/;##]
-      ##|#ltjkn;
-         ncut (O < n); ##[/2/; ##] #posn;
-         ncut (k ≤ n); ##[/2/; ##] #lekn;
-         nrewrite > (lt_to_leb_false (S (n-1)) k ?); nnormalize;
-          ##[nrewrite > (lt_to_leb_false … (le_S_S … lekn));
-             nrewrite > (subst_rel3 A (j+k+1) (n+1) ?);
-              ##[nrewrite < (plus_minus_m_m … posn);//;
-              ##|napplyS monotonic_lt_plus_l; //;
-              ##]
-          ##|napply le_S_S; 
-             napply (not_eq_to_le_to_le_minus … lekn);
-             /2/; (* come fa? *)
-          ##]
-     ##]
-  ##]
-nqed. *)
-
-naxiom lift_subst_aux_kij: ∀A,B.∀i,j,k.
-  lift_aux (subst_aux B (j+k) A) k i = subst_aux (lift_aux B k i) (j+k+i) A.
-
-nlemma lift_subst_aux_k: ∀A,B.∀j,k.
-  lift_aux (subst_aux B (j+k) A) k 1 = subst_aux (lift_aux B k 1) (S(j+k)) A.
-#A; #B; #j; nelim B; nnormalize; /2/; #n; #k;
-napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk;
-  ##[nelim (leb (S n) k); 
-    ##[nrewrite > (subst_rel1 A (S(j+k)) n ?);/2/;
-    ##|nrewrite > (subst_rel1 A (S(j+k)) (n+1) ?);/2/;
-    ##]
-  ##|napply (eqb_elim n (j+k)); nnormalize; #Heqnjk; 
-    ##[nrewrite > (lt_to_leb_false (S n) k ?);
-       ##[ncut (S(j+k) = n+1);##[//;##] #Heq;
-          nrewrite > Heq; nrewrite > (subst_rel2 A ?); nnormalize;
-          napplyS lift_lift_aux2 (* bello *);//;
-       ##|/2/;
-       ##]
-    ##|ncut (j + k < n);
-      ##[napply not_eq_to_le_to_lt;
-        ##[/2/;##|napply le_S_S_to_le;napply not_le_to_lt;/2/;##]
-      ##|#ltjkn;
-         ncut (O < n); ##[/2/; ##] #posn;
-         ncut (k ≤ n); ##[/2/; ##] #lekn;
-         nrewrite > (lt_to_leb_false (S (n-1)) k ?); nnormalize;
-          ##[nrewrite > (lt_to_leb_false … (le_S_S … lekn));
-             nrewrite > (subst_rel3 A (S(j+k)) (n+1) ?);
-              ##[nrewrite < (plus_minus_m_m … posn);//;
-              ##|ncut (S n = n +1); /2/;
-              ##]
-          ##|napply le_S_S;  (* /3/;*)
-             napply (not_eq_to_le_to_le_minus … lekn);
-             /3/; (* come fa? *)
-          ##]
-     ##]
-  ##]
-nqed. 
-
-(*
-nlemma lift_subst_aux_k: ∀A,B.∀k. 
-  lift_aux (subst_aux B k A) k 1 = subst_aux (lift_aux B k 1) (k+1) A.
-#A; #B; nelim B; nnormalize; /2/; #n; #k;
-napply (leb_elim (S n) k); nnormalize; #Hnk;
-  ##[nrewrite > (le_to_leb_true ?? Hnk);
-     nrewrite > (le_to_leb_true (S n) (k +1) ?);nnormalize;/2/;
-  ##|nrewrite > (lt_to_leb_false (S (n + 1)) (k+1) ?);
-    ##[##2: napply le_S_S; napply (monotonic_le_plus_l 1 k n);
-       napply not_lt_to_le; napply Hnk; ##]      
-    napply (eqb_elim n k);#eqnk;
-      ##[nrewrite > (eq_to_eqb_true (n+1) (k+1) ?);/2/;
-         nnormalize; nrewrite < eqnk; //; (* strano *)
-      ##|nrewrite > (not_eq_to_eqb_false (n+1) (k+1) ?);/2/;
-         nnormalize; 
-         ncut (O < n);
-          ##[napply not_le_to_lt;#len;
-             napply eqnk; napply le_to_le_to_eq;
-              ##[napply transitive_le; //;
-              ##|napply not_lt_to_le; /2/;
-              ##] 
-          ##|#posn;
-             nrewrite > (lt_to_leb_false (S (n - 1)) k ?);
-             ##[nnormalize;
-                (* nrewrite < (minus_plus_m_m n 1); *)
-                nrewrite < (plus_minus_m_m n 1 ?);//;
-             ##|napply le_S_S; napply not_eq_to_le_to_le_minus;
-                ##[/2/;
-                ##|napply (not_lt_to_le … Hnk);
-                ##]
-             ##]
-          ##]
-       ##]
-  ##]
-nqed.
 *)
 
-ntheorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k → 
-  subst_aux (lift_aux B i (S k)) j A = (lift_aux B i k).
-#A; #B; nelim B; nnormalize; /2/;
-   ##[##2,3,4: #T; #T0; #Hind1; #Hind2; #i; #j; #k; #leij; #lejk;
-      napply eq_f2;/2/; napply Hind2;
-      napplyS (monotonic_le_plus_l 1);//
-   ##|#n; #i; #j; #k; #leij; #ltjk;
-      napply (leb_elim (S n) i); nnormalize; #len;
-      ##[nrewrite > (le_to_leb_true (S n) j ?);/2/;
-      ##|nrewrite > (lt_to_leb_false (S (n+S k)) j ?);
-        ##[nnormalize; 
-           nrewrite > (not_eq_to_eqb_false (n+S k) j ?);
-           nnormalize; /2/; napply (not_to_not …len);
-           #H; napply (le_plus_to_le_r k); (* why napplyS ltjk; *)
-           nnormalize; //; 
-        ##|napply le_S_S; napply (transitive_le … ltjk);
-           napply le_plus;//; napply not_lt_to_le; /2/;
-        ##]
-    ##]
-nqed.
-     
-(********************* substitution lemma ***********************)    
-nlemma subst_lemma: ∀A,B,C.∀k,i. 
-  subst_aux (subst_aux A i B) (k+i) C = 
-    subst_aux (subst_aux A (S (k+i)) C) i (subst_aux B k C).
-#A; #B; #C; #k; nelim A; nnormalize;//; (* WOW *)
-#n; #i; napply (leb_elim (S n) i); #Hle;
-  ##[ncut (n < k+i); ##[/2/##] #ltn; (* lento *)
-     ncut (n ≤ k+i); ##[/2/##] #len;
-     nrewrite > (subst_rel1 C (k+i) n ltn);
-     nrewrite > (le_to_leb_true n (k+i) len);
-     nrewrite > (subst_rel1 … Hle);//;
-  ##|napply (eqb_elim n i); #eqni;
-    ##[nrewrite > eqni; 
-       nrewrite > (le_to_leb_true i (k+i) ?); //;
-       nrewrite > (subst_rel2 …); nnormalize; 
-       napply symmetric_eq; 
-       napplyS (lift_subst_aux_kij C B i k O);
-    ##|napply (leb_elim (S (n-1)) (k+i)); #nk;
-      ##[nrewrite > (subst_rel1 C (k+i) (n-1) nk);
-         nrewrite > (le_to_leb_true n (k+i) ?);
-        ##[nrewrite > (subst_rel3 ? i n ?);//;
-           napply not_eq_to_le_to_lt;
-            ##[/2/;
-            ##|napply not_lt_to_le;/2/;
-            ##]
-        ##|napply (transitive_le … nk);//;
-        ##]
-      ##|ncut (i < n);
-        ##[napply not_eq_to_le_to_lt; ##[/2/]
-           napply (not_lt_to_le … Hle);##]
-         #ltin; ncut (O < n); ##[/2/;##] #posn;
-         napply (eqb_elim (n-1) (k+i)); #H
-         ##[nrewrite > H; nrewrite > (subst_rel2 C (k+i));
-            nrewrite > (lt_to_leb_false n (k+i) ?);
-            ##[nrewrite > (eq_to_eqb_true n (S(k+i)) ?); 
-              ##[nnormalize;
-              ##|nrewrite < H; napplyS plus_minus_m_m;//;
-              ##]
-            ##|nrewrite < H; napply (lt_O_n_elim … posn);
-               #m; nnormalize;//;
-            ##]
-         ##|ncut (k+i < n-1);
-            ##[napply not_eq_to_le_to_lt;
-              ##[napply symmetric_not_eq; napply H;
-              ##|napply (not_lt_to_le … nk);
-              ##]
-            ##]
-            #Hlt; nrewrite > (lt_to_leb_false n (k+i) ?);
-            ##[nrewrite > (not_eq_to_eqb_false n (S(k+i)) ?);
-              ##[nrewrite > (subst_rel3 C (k+i) (n-1) Hlt);
-                 nrewrite > (subst_rel3 ? i (n-1) ?);//;
-                 napply (le_to_lt_to_lt … Hlt);//;
-              ##|napply (not_to_not … H); #Hn; nrewrite > Hn; nnormalize;//;
-              ##]
-            ##|napply (transitive_lt … Hlt);
-               napply (lt_O_n_elim … posn);
-               #m; nnormalize;//;
-            ##]
-          ##]
-          nrewrite <H;
-          ncut (∃m:nat. S m = n);
-          ##[napply (lt_O_n_elim … posn); #m;@ m;//;
-            ##|*; #m; #Hm; nrewrite < Hm;
-               nrewrite > (delift ???????);nnormalize;/2/;
-          ##]
-nqed.
-  
-(*************************** substl *****************************)
-
-nlet rec substl (G:list T) (N:T) : list T ≝  
-  match G with
-    [ nil ⇒ nil T
-    | cons A D ⇒ ((subst_aux A (length T D) N)::(substl D N))
-    ].
-    
+(*
+nlemma length_cons: ∀A.∀G. length T (A::G) = length T G + 1.
+/2/; nqed.*)
 
-(*****************************************************************)
+(****************************************************************)
 
 naxiom A: nat → nat → Prop.
 naxiom R: nat → nat → nat → Prop.
 naxiom conv: T → T → Prop.
 
 ninductive TJ: list T → T → T → Prop ≝
-  | ax : ∀i,j. A i j → TJ [] (Sort i) (Sort j)
-  | start: ∀G.∀A.∀i.TJ G A (Sort i) → TJ (A::G) (Rel 0) (lift A 1)
+  | ax : ∀i,j. A i j → TJ (nil T) (Sort i) (Sort j)
+  | start: ∀G.∀A.∀i.TJ G A (Sort i) → TJ (A::G) (Rel 0) (lift A 0 1)
   | weak: ∀G.∀A,B,C.∀i.
-     TJ G A B → TJ G C (Sort i) → TJ (C::G) (lift A 1) (lift B 1)
+     TJ G A B → TJ G C (Sort i) → TJ (C::G) (lift A 0 1) (lift B 0 1)
   | prod: ∀G.∀A,B.∀i,j,k. R i j k →
      TJ G A (Sort i) → TJ (A::G) B (Sort j) → TJ G (Prod A B) (Sort k)
   | app: ∀G.∀F,A,B,a. 
-     TJ G F (Prod A B) → TJ G a A → TJ G (App F a) (subst B a)
+     TJ G F (Prod A B) → TJ G a A → TJ G (App F a) (subst B 0 a)
   | abs: ∀G.∀A,B,b.∀i. 
      TJ (A::G) b B → TJ G (Prod A B) (Sort i) → TJ G (Lambda A b) (Prod A B)
   | conv: ∀G.∀A,B,C.∀i. conv B C →
      TJ G A B → TJ G B (Sort i) → TJ G A C.
- 
-ninverter TJ_inv2 for TJ (%?%) : Prop.
+     
+notation "hvbox(G break  ⊢ A : B)" non associative with precedence 50 for @{'TJ $G $A $B}.
+interpretation "type judgement" 'TJ G A B = (TJ G A B).
+
+(* ninverter TJ_inv2 for TJ (%?%) : Prop. *)
 
 (**** definitions ****)
 
 ninductive Glegal (G: list T) : Prop ≝
-glegalk : ∀A,B.TJ G A B → Glegal G.
+glegalk : ∀A,B. G ⊢ A : B → Glegal G.
 
 ninductive Gterm (G: list T) (A:T) : Prop ≝
-  | is_term: ∀B.TJ G A B → Gterm G A
-  | is_type: ∀B.TJ G B A → Gterm G A.
+  | is_term: ∀B.G ⊢ A:B → Gterm G A
+  | is_type: ∀B.G ⊢ B:A → Gterm G A.
 
 ninductive Gtype (G: list T) (A:T) : Prop ≝ 
-gtypek: ∀i.TJ G A (Sort i) → Gtype G A.
+gtypek: ∀i.G ⊢ A : Sort i → Gtype G A.
 
 ninductive Gelement (G:list T) (A:T) : Prop ≝
-gelementk: ∀B.TJ G A B → Gtype G B → Gelement G A.
+gelementk: ∀B.G ⊢ A:B → Gtype G B → Gelement G A.
 
 ninductive Tlegal (A:T) : Prop ≝ 
 tlegalk: ∀G. Gterm G A → Tlegal A.
@@ -423,13 +95,13 @@ subst C A
 *)
 
 ntheorem start_lemma1: ∀G.∀i,j. 
-A i j → Glegal G → TJ G (Sort i) (Sort j).
+A i j → Glegal G → G ⊢ Sort i: Sort j.
 #G; #i; #j; #axij; #Gleg; ncases Gleg; 
 #A; #B; #tjAB; nelim tjAB; /2/;
 (* bello *) nqed.
 
 ntheorem start_rel: ∀G.∀A.∀C.∀n,i,q.
-TJ G C (Sort q) → TJ G (Rel n) (lift A i) → TJ (C::G) (Rel (S n)) (lift A (S i)).
+G ⊢ C: Sort q → G ⊢ Rel n: lift A 0 i → (C::G) ⊢ Rel (S n): lift A 0 (S i).
 #G; #A; #C; #n; #i; #p; #tjC; #tjn;
  napplyS (weak G (Rel n));//. (* bello *)
  (*
@@ -441,7 +113,7 @@ TJ G C (Sort q) → TJ G (Rel n) (lift A i) → TJ (C::G) (Rel (S n)) (lift A (S
 nqed.
   
 ntheorem start_lemma2: ∀G.
-Glegal G → ∀n. n < length T G → TJ G (Rel n) (lift (nth n T G (Rel O)) (S n)).
+Glegal G → ∀n. n < |G| → G ⊢ Rel n: lift (nth n T G (Rel O)) 0 (S n).
 #G; #Gleg; ncases Gleg; #A; #B; #tjAB; nelim tjAB; /2/;
   ##[#i; #j; #axij; #p; nnormalize; #abs; napply False_ind;
      napply (absurd … abs); //; 
@@ -493,8 +165,8 @@ ntheorem substitution_tj:
 *)
 
 ntheorem substitution_tj: 
-∀E.∀A,B,M.TJ E M B → ∀G,D.∀N. E = D@A::G → TJ G N A → 
-  TJ ((substl D N)@G) (subst_aux M (length ? D) N) (subst_aux B (length ? D) N).
+∀E.∀A,B,M. E ⊢M:B → ∀G,D.∀N. E = D@A::G → G ⊢ N:A → 
+  ((substl D N)@G) ⊢ M[|D| ← N]: B[|D| ← N].
 #E; #A; #B; #M; #tjMB; nelim tjMB; 
   ##[nnormalize; #i; #j; #k; #G; #D; #N; ncases D; 
       ##[nnormalize; #isnil; ndestruct;
@@ -502,70 +174,46 @@ ntheorem substitution_tj:
       ##]
   ##|#G; #A1; #i; #tjA; #Hind; #G1; #D; ncases D; 
     ##[#N; #Heq; #tjN; 
-       nrewrite > (delift (lift N O) A1 O O O ??); //;
+       nrewrite > (delift (lift N O O) A1 O O O ??); //;
        nnormalize in Heq; ndestruct;/2/;
     ##|#H; #L; #N1; #Heq; nnormalize in Heq;
-       #tjN1; nnormalize; ndestruct;
-       (* porcherie *)
-       ncut (S (length T L) = S ((length T L)+0)); ##[//##] #Heq;
-       nrewrite > Heq;
-       nrewrite < (lift_subst_aux_k N1 H (length T L) O);
-       nrewrite < (plus_n_O (length T L));
-       napply start;/2/;
+       #tjN1; nnormalize; ndestruct;             
+       napplyS start; /2/;
     ##]
   ##|#G; #P; #Q; #R; #i; #tjP; #tjR; #Hind1; #Hind2;
      #G1; #D; #N; ncases D; nnormalize;
     ##[#Heq; ndestruct; #tjN; //;
     ##|#H; #L; #Heq;
        #tjN1; ndestruct;
-       (* porcherie *)
-       ncut (S (length T L) = S ((length T L)+0)); ##[//##] #Heq;
-       nrewrite > Heq;
-       nrewrite < (lift_subst_aux_k N P (length T L) O);
-       nrewrite < (lift_subst_aux_k N Q (length T L) O);
-       nrewrite < (plus_n_O (length T L));
-       napply weak;/2/;
+       (* napplyS weak non va *)
+       ncut (S (length T L) = (length T L)+0+1); ##[//##] #Heq;
+       napplyS weak; /2/;
     ##]
   ##|#G; #P; #Q; #i; #j; #k; #Ax; #tjP; #tjQ; #Hind1; #Hind2;
-     #G1; #D; #N; #Heq; #tjN;
+     #G1; #D; #N; #Heq; #tjN; nnormalize;
      napply (prod … Ax); 
     ##[/2/;
-    ##|
+    ##|ncut (S (length T D) = (length T D)+1); ##[//##] #Heq1;
+       nrewrite < Heq1; 
+       napply (Hind2 ? (P::D));nnormalize;//;
     ##]
   ##|#G; #P; #Q; #R; #S; #tjP; #tjS; #Hind1; #Hind2;
+     #G1; #D; #N; #Heq; #tjN; nnormalize in Hind1 ⊢ %;
+     nrewrite > (plus_n_O (length ? D)) in ⊢ (? ? ? (? ? % ?));
+     nrewrite > (subst_lemma R S N ? 0);
+     napplyS app; /2/;
+  ##|#G; #P; #Q; #R; #i; #tjR; #tjProd; #Hind1; #Hind2;
      #G1; #D; #N; #Heq; #tjN; nnormalize;
-     ncheck app.
-  
+     napplyS abs; 
+      ##[nnormalize in Hind2; /2/;
+      ##|(* napplyS (Hind1 G1 (P::D) N ? tjN); sistemare *)
+       ngeneralize in match (Hind1 G1 (P::D) N ? tjN); 
+        ##[#H; nnormalize in H; napplyS H;##|nnormalize; //##]
+      ##|##]
+  ##|
+ 
   
-       
-       
-ntheorem substitution_tj: 
-∀E.∀A,B,M.TJ E M B → ∀G,D.∀N. E = D@A::G → TJ G N A → 
-∀k.length ? D = k →
-  TJ ((substl D N)@G) (subst_aux M k N) (subst_aux B k N).
-#E; #A; #B; #M; #tjMB; nelim tjMB; 
-  ##[nnormalize; (* /3/; *)
-  ##|#G; #A1; #i; #tjA; #Hind; 
-     #G1; #D; ncases D; 
-    ##[#N; #Heq; #tjN; #k; nnormalize in ⊢ (% → ?); #kO; 
-       nrewrite < kO;
-       nrewrite > (delift (lift N O) A1 O O O ??); //;
-       nnormalize in Heq; ndestruct;/2/;
-    ##|#H; #L; #N1; #Heq; nnormalize in Heq;
-       #tjN1; #k; #len; nnormalize in len;
-       nrewrite < len; 
-       nnormalize; ndestruct;
-       (* porcherie *)
-       ncut (S (length T L) = S ((length T L)+0)); ##[//##] #Heq;
-       nrewrite > Heq;
-       nrewrite < (lift_subst_aux_k N1 H (length T L) O);
-       nrewrite < (plus_n_O (length T L));
-       napply (start (substl L N1@G1) (subst_aux H (length T L) N1) i ?).
-       napply Hind;//;
-    ##]
-       
-
-
+