X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Flambda%2Ftypes.ma;h=d8ddb19239f1747b74df366bddcd75f973d22645;hb=589abc887494582fb011df38897bb142d6da42c9;hp=09ecd4e05e7e9a3cb488b63c70c2688f06952cf1;hpb=6bbf27282bad84e066bb952e41dbc8f72b31de6c;p=helm.git

diff --git a/matita/matita/lib/lambda/types.ma b/matita/matita/lib/lambda/types.ma
index 09ecd4e05..d8ddb1923 100644
--- a/matita/matita/lib/lambda/types.ma
+++ b/matita/matita/lib/lambda/types.ma
@@ -27,32 +27,52 @@ substl (A::G) N = (subst_aux A (length T G) N)::(substl G N).
 //; nqed.
 *)
 
-(*
+(*start: ∀G.∀A.∀i.TJ G A (Sort i) → TJ (A::G) (Rel 0) (lift A 0 1)
+  | 
 nlemma length_cons: ∀A.∀G. length T (A::G) = length T G + 1.
 /2/; nqed.*)
 
 (****************************************************************)
 
+(*
 axiom A: nat → nat → Prop.
 axiom R: nat → nat → nat → Prop.
-axiom conv: T → T → Prop.
-
-inductive 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 0 1)
+axiom conv: T → T → Prop.*)
+
+inductive TJ 
+ (S: nat → nat → Prop)
+ (R: nat → nat → nat → Prop)
+ (c: T → T → Prop) : list T → T → T → Prop ≝
+  | ax : ∀i,j. S i j → TJ S R c (nil T) (Sort i) (Sort j)
+  | start: ∀G.∀A.∀i.TJ S R c G A (Sort i) → 
+      TJ S R c (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 0 1) (lift B 0 1)
+     TJ S R c G A B → TJ S R c G C (Sort i) → 
+       TJ S R c (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)
+     TJ S R c G A (Sort i) → TJ S R c (A::G) B (Sort j) → 
+       TJ S R c 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 0 a)
+     TJ S R c G F (Prod A B) → TJ S R c G a A → 
+       TJ S R c 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.
+     TJ S R c (A::G) b B → TJ S R c G (Prod A B) (Sort i) → 
+       TJ S R c G (Lambda A b) (Prod A B)
+  | conv: ∀G.∀A,B,C.∀i. c B C →
+     TJ S R c G A B → TJ S R c G C (Sort i) → TJ S R c G A C
+  | dummy: ∀G.∀A,B.∀i. 
+     TJ S R c G A B → TJ S R c G B (Sort i) → TJ S R c G (D A) B.
      
-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).
+interpretation "type judgement" 'TJ G A B = (TJ ? ? ? G A B).
+
+record pts : Type[0] ≝ {
+  s1: nat → nat → Prop;
+  r1: nat → nat → nat → Prop;
+  c1: T → T → Prop
+  }.
+
+check r1.
+definition TJ ≝ λp:pts.c p. 
 
 (* ninverter TJ_inv2 for TJ (%?%) : Prop. *)
 
@@ -114,7 +134,7 @@ qed.
 theorem start_lemma2: ∀G.
 Glegal G → ∀n. n < |G| → G ⊢ Rel n: lift (nth n T G (Rel O)) 0 (S n).
 #G #Gleg (cases Gleg) #A #B #tjAB (elim tjAB) /2/
-  [#i #j #axij #p normalize #abs @False_ind @(absurd … abs) // 
+  [#i #j #axij #p normalize #abs @(False_ind) @(absurd … abs) // 
   |#G #A #i #tjA #Hind #m (cases m) /2/
    #p #Hle @start_rel // @Hind @le_S_S_to_le @Hle
   |#G #A #B #C #i #tjAB #tjC #Hind1 #_ #m (cases m)
@@ -204,16 +224,15 @@ theorem substitution_tj:
       [#H (normalize in H) (applyS H) | normalize // ]
     ]
   |#G #P #Q #R #i #convQR #tjP #tjQ #Hind1 #Hind2
-   #G1 #D #N #Heq #tjN (normalize in Hind1 ⊢ %)
-   @(conv …(conv_subst … convQR) ? (Hind2 …)) //
-   @Hind1 //
+   #G1 #D #N #Heq #tjN
+   @(conv …(conv_subst … convQR) ? (Hind2 …)) // @Hind1 //
+  |#G #P #Q #i #tjP #tjQ #Hind1 #Hind2
+   #G1 #D #N #Heq #tjN @dummy /2/ 
   ]
 qed.
- 
-  
- 
-
-
-
-
 
+lemma tj_subst_0: ∀G,v,w. G ⊢ v : w → ∀t,u. w :: G ⊢ t : u →
+                  G ⊢ t[0≝v] : u[0≝v].
+#G #v #w #Hv #t #u #Ht 
+lapply (substitution_tj … Ht ? ([]) … Hv) normalize //
+qed.