From c8ec2f3e2aaa71efa702f86bacc95e393778a56f Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 17 Mar 2010 14:58:51 +0000
Subject: [PATCH] qualche caso del lemma 5.2.11

---
 helm/software/matita/nlibrary/PTS/gpts.ma | 28 ++++++++++++++++++-----
 1 file changed, 22 insertions(+), 6 deletions(-)

diff --git a/helm/software/matita/nlibrary/PTS/gpts.ma b/helm/software/matita/nlibrary/PTS/gpts.ma
index c6aeb1bd4..d43efef3f 100644
--- a/helm/software/matita/nlibrary/PTS/gpts.ma
+++ b/helm/software/matita/nlibrary/PTS/gpts.ma
@@ -21,7 +21,16 @@ nlet rec substl (G:list T) (N:T) : list T ≝
     [ nil ⇒ nil T
     | cons A D ⇒ ((subst_aux A (length T D) N)::(substl D N))
     ].
-    
+
+(*
+nlemma substl_cons: ∀A,N.∀G.
+substl (A::G) N = (subst_aux A (length T G) N)::(substl G N).
+//; nqed.
+
+nlemma length_cons: ∀A.∀G. length T (A::G) = length T G + 1.
+/2/; nqed.
+*)
+
 (****************************************************************)
 
 naxiom A: nat → nat → Prop.
@@ -31,6 +40,8 @@ naxiom conv: T → T → Prop.
 nlemma mah: ∀A,i. lift A i = lift_aux A 0 i.
 //; nqed.
 
+ncheck subst.
+
 ninductive TJ: list T → T → T → Prop ≝
   | 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 1)
@@ -39,7 +50,7 @@ ninductive TJ: list T → T → T → Prop ≝
   | 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 a B)
   | 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 →
@@ -188,13 +199,18 @@ ntheorem substitution_tj:
      #G1; #D; #N; #Heq; #tjN; nnormalize;
      napply (prod … Ax); 
     ##[/2/;
-    ##|(* metas not found *)
-       napplyS (Hind2 G1 (P::D) N );
-       nnormalize;
+    ##|ncheck (Hind2 G1 (P::D) N ? tjN).
+       ncut (S (length T D) = (length T D)+1); ##[//##] #Heq1;
+       nrewrite < Heq1;
+       napply (Hind2 ? (P::D));//;
     ##]
   ##|#G; #P; #Q; #R; #S; #tjP; #tjS; #Hind1; #Hind2;
      #G1; #D; #N; #Heq; #tjN; nnormalize;
-     ncheck app.
+     nlapply (subst_lemma R S N (length ? D) 0); #sl;
+     nrewrite < (plus_n_O ?) in sl; #sl;
+     nrewrite > sl;
+     napply app; nnormalize in Hind1;/2/;
+  ##|
   
   
        
-- 
2.39.2