helm/software/matita/nlibrary/PTS/gpts.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "basics/list2.ma".
  16
  17 ninductive T : Type ≝
  18   | Sort: nat → T
  19   | Rel: nat → T
  20   | App: T → T → T
  21   | Lambda: T → T → T (* type, body *)
  22   | Prod: T → T → T (* type, body *)
  23 .
  24
  25 nlet rec lift_aux t k p ≝
  26   match t with
  27     [ Sort n ⇒ Sort n
  28     | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n) (Rel (n+p))
  29     | App m n ⇒ App (lift_aux m k p) (lift_aux n k p)
  30     | Lambda m n ⇒ Lambda (lift_aux m k p) (lift_aux n (k+1) p)
  31     | Prod m n ⇒ Prod (lift_aux m k p) (lift_aux n (k+1) p)
  32     ].
  33
  34 ndefinition lift ≝ λt.λp.lift_aux t 0 p.
  35
  36 nlet rec subst_aux t k a ≝
  37   match t with
  38     [ Sort n ⇒ Sort n
  39     | Rel n ⇒ if_then_else T (leb (S n) k) (Rel n)
  40         (if_then_else T (eqb n k) (lift a n) (Rel (n-1)))
  41     | App m n ⇒ App (subst_aux m k a) (subst_aux n k a)
  42     | Lambda m n ⇒ Lambda (subst_aux m k a) (subst_aux n (k+1) a)
  43     | Prod m n ⇒ Prod (subst_aux m k a) (subst_aux n (k+1) a)
  44     ].
  45
  46 ndefinition subst ≝ λa.λt.subst_aux t 0 a.
  47
  48 (*** properties of lift and subst ***)
  49 nlemma lift_aux_0: ∀t:T.∀k. lift_aux t k 0 = t.
  50 #t; nelim t; nnormalize; //; #n; #k; ncases (leb (S n) k);
  51 nnormalize;//;nqed.
  52
  53 nlemma lift_0: ∀t:T. lift t 0 = t.
  54 #t; nelim t; nnormalize; //; nqed.
  55
  56 nlemma lift_sort: ∀i,k. lift (Sort i) k = Sort i.
  57 //; nqed.
  58
  59 nlemma lift_rel: ∀i,k. lift (Rel i) k = Rel (i+k).
  60 //; nqed.
  61
  62 nlemma lift_rel1: ∀i.lift (Rel i) 1 = Rel (S i).
  63 #i; nchange with (lift (Rel i) 1 = Rel (1 + i)); //; nqed.
  64
  65 (*
  66 nlemma lift_lift_aux: ∀t.∀i,j,k,k1. k ≤ k1 → k1 ≤ k+j →
  67 lift_aux (lift_aux t k j) k1 i = lift_aux t k (j+i).
  68 #t; nelim t; nnormalize; //; #n; #i;#j; #k; #k1; #lel; #ler;
  69 napply (leb_elim (S n) k); #Hnk;nnormalize;
  70   ##[nrewrite > (le_to_leb_true ? ? Hnk);nnormalize;//;
  71   ##|nrewrite > (lt_to_leb_false (S n+j) k ?);
  72      nnormalize;//;napply (lt_to_le_to_lt ? (S n));
  73       ##[napply not_le_to_lt;/2/;
  74       ##|(* lento /2/; *) napply le_S_S;/1/;
  75   ##]
  76 nqed. *)
  77
  78 nlemma lift_lift_aux: ∀t.∀i,j,k. lift_aux (lift_aux t k j) k i = lift_aux t k (j+i).
  79 #t; nelim t; nnormalize; //; #n; #i;#j; #k;
  80 napply (leb_elim (S n) k); #Hnk;nnormalize;
  81   ##[nrewrite > (le_to_leb_true ? ? Hnk);nnormalize;//;
  82   ##|nrewrite > (lt_to_leb_false (S n+j) k ?);
  83      nnormalize;//; napply (lt_to_le_to_lt ? (S n));
  84       ##[napply not_le_to_lt;//;
  85       ##|napply le_S_S;//;
  86   ##]
  87 nqed.
  88
  89 nlemma lift_lift_aux1: ∀t.∀i,j,k. lift_aux (lift_aux t k j) (j+k) i = lift_aux t k (j+i).
  90 #t; nelim t; nnormalize; //; #n; #i;#j; #k;
  91 napply (leb_elim (S n) k); #Hnk;nnormalize;
  92   ##[nrewrite > (le_to_leb_true (S n) (j+k) ?);nnormalize;/2/;
  93   ##|nrewrite > (lt_to_leb_false (S n+j) (j+k) ?);
  94      nnormalize;//; napply le_S_S; napplyS monotonic_le_plus_r;
  95      /3/;
  96   ##]
  97 nqed.
  98
  99 nlemma lift_lift_aux2: ∀t.∀i,j.j ≤ i  → ∀h,k.
 100 lift_aux (lift_aux t k i) (j+k) h = lift_aux t k (i+h).
 101 #t; #i; #j; #h; nelim t; nnormalize; //; #n; #h;#k;
 102 napply (leb_elim (S n) k); #Hnk;nnormalize;
 103   ##[nrewrite > (le_to_leb_true (S n) (j+k) ?);nnormalize;/2/;
 104   ##|nrewrite > (lt_to_leb_false (S n+i) (j+k) ?);
 105      nnormalize;//;napply le_S_S; nrewrite > (symmetric_plus j k);
 106      napply le_plus;//;napply not_lt_to_le;/2/;
 107   ##]
 108 nqed.
 109
 110 nlemma lift_lift: ∀t.∀i,j. lift (lift t j) i = lift t (j+i).
 111 nnormalize; //;
 112 nqed.
 113
 114 nlemma subst_lift_aux_k: ∀A,B.∀k.
 115   subst_aux (lift_aux B k 1) k A = B.
 116 #A; #B; nelim B; nnormalize; /2/; #n; #k;
 117 napply (leb_elim (S n) k); nnormalize; #Hnk;
 118   ##[nrewrite > (le_to_leb_true ?? Hnk);nnormalize;//;
 119   ##|nrewrite > (lt_to_leb_false (S (n + 1)) k ?); nnormalize;
 120       ##[nrewrite > (not_eq_to_eqb_false (n+1) k ?);
 121          nnormalize;/2/; napply (not_to_not … Hnk);//;
 122       ##|napply le_S; napplyS (not_le_to_lt (S n) k Hnk);
 123       ##]
 124   ##]
 125 nqed.
 126
 127 nlemma subst_lift: ∀A,B. subst A (lift B 1) = B.
 128 nnormalize; //; nqed.
 129
 130 nlemma subst_aux_sort: ∀A.∀n,k. subst_aux (Sort n) k A = Sort n.
 131 //; nqed.
 132
 133 nlemma subst_sort: ∀A.∀n. subst A (Sort n) = Sort n.
 134 //; nqed.
 135
 136 nlemma subst_rel: ∀A.subst A (Rel O) = A.
 137 nnormalize; //; nqed.
 138
 139 nlemma subst_rel1: ∀A.∀k,i. i < k →
 140   subst_aux (Rel i) k A = Rel i.
 141 #A; #k; #i; nnormalize; #ltik;
 142 nrewrite > (le_to_leb_true (S i) k ?); //; nqed.
 143
 144 nlemma subst_rel2: ∀A.∀k. subst_aux (Rel k) k A = lift A k.
 145 #A; #k; nnormalize;
 146 nrewrite > (lt_to_leb_false (S k) k ?); //;
 147 nrewrite > (eq_to_eqb_true … (refl …)); //;
 148 nqed.
 149
 150 nlemma subst_rel3: ∀A.∀k,i. k < i →
 151   subst_aux (Rel i) k A = Rel (i-1).
 152 #A; #k; #i; nnormalize; #ltik;
 153 nrewrite > (lt_to_leb_false (S i) k ?); /2/;
 154 nrewrite > (not_eq_to_eqb_false i k ?); //;
 155 napply nmk; #eqik; nelim (lt_to_not_eq … (ltik …)); /2/;
 156 nqed.
 157
 158 (* versione con plus
 159 nlemma lift_subst_aux_k: ∀A,B.∀j,k.
 160   lift_aux (subst_aux B (j+k) A) k 1 = subst_aux (lift_aux B k 1) (j+k+1) A.
 161 #A; #B; #j; nelim B; nnormalize; /2/; #n; #k;
 162 napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk;
 163   ##[nelim (leb (S n) k);
 164     ##[nrewrite > (subst_rel1 A (j+k+1) n ?);/2/;
 165     ##|nrewrite > (subst_rel1 A (j+k+1) (n+1) ?);/2/;
 166     ##]
 167   ##|napply (eqb_elim n (j+k)); nnormalize; #Heqnjk;
 168     ##[nrewrite > (lt_to_leb_false (S n) k ?);
 169        ##[ncut (j+k+1 = n+1);##[//;##] #Heq;
 170           nrewrite > Heq; nrewrite > (subst_rel2 A ?); nnormalize;
 171           napplyS lift_lift_aux2 (* bello *);//;
 172        ##|/2/;
 173        ##]
 174     ##|ncut (j + k < n);
 175       ##[napply not_eq_to_le_to_lt;
 176         ##[/2/;##|napply le_S_S_to_le;napply not_le_to_lt;/2/;##]
 177       ##|#ltjkn;
 178          ncut (O < n); ##[/2/; ##] #posn;
 179          ncut (k ≤ n); ##[/2/; ##] #lekn;
 180          nrewrite > (lt_to_leb_false (S (n-1)) k ?); nnormalize;
 181           ##[nrewrite > (lt_to_leb_false … (le_S_S … lekn));
 182              nrewrite > (subst_rel3 A (j+k+1) (n+1) ?);
 183               ##[nrewrite < (plus_minus_m_m … posn);//;
 184               ##|napplyS monotonic_lt_plus_l; //;
 185               ##]
 186           ##|napply le_S_S;
 187              napply (not_eq_to_le_to_le_minus … lekn);
 188              /2/; (* come fa? *)
 189           ##]
 190      ##]
 191   ##]
 192 nqed. *)
 193
 194 naxiom lift_subst_aux_kij: ∀A,B.∀i,j,k.
 195   lift_aux (subst_aux B (j+k) A) k i = subst_aux (lift_aux B k i) (j+k+i) A.
 196
 197 nlemma lift_subst_aux_k: ∀A,B.∀j,k.
 198   lift_aux (subst_aux B (j+k) A) k 1 = subst_aux (lift_aux B k 1) (S(j+k)) A.
 199 #A; #B; #j; nelim B; nnormalize; /2/; #n; #k;
 200 napply (leb_elim (S n) (j + k)); nnormalize; #Hnjk;
 201   ##[nelim (leb (S n) k);
 202     ##[nrewrite > (subst_rel1 A (S(j+k)) n ?);/2/;
 203     ##|nrewrite > (subst_rel1 A (S(j+k)) (n+1) ?);/2/;
 204     ##]
 205   ##|napply (eqb_elim n (j+k)); nnormalize; #Heqnjk;
 206     ##[nrewrite > (lt_to_leb_false (S n) k ?);
 207        ##[ncut (S(j+k) = n+1);##[//;##] #Heq;
 208           nrewrite > Heq; nrewrite > (subst_rel2 A ?); nnormalize;
 209           napplyS lift_lift_aux2 (* bello *);//;
 210        ##|/2/;
 211        ##]
 212     ##|ncut (j + k < n);
 213       ##[napply not_eq_to_le_to_lt;
 214         ##[/2/;##|napply le_S_S_to_le;napply not_le_to_lt;/2/;##]
 215       ##|#ltjkn;
 216          ncut (O < n); ##[/2/; ##] #posn;
 217          ncut (k ≤ n); ##[/2/; ##] #lekn;
 218          nrewrite > (lt_to_leb_false (S (n-1)) k ?); nnormalize;
 219           ##[nrewrite > (lt_to_leb_false … (le_S_S … lekn));
 220              nrewrite > (subst_rel3 A (S(j+k)) (n+1) ?);
 221               ##[nrewrite < (plus_minus_m_m … posn);//;
 222               ##|ncut (S n = n +1); /2/;
 223               ##]
 224           ##|napply le_S_S;  (* /3/;*)
 225              napply (not_eq_to_le_to_le_minus … lekn);
 226              /3/; (* come fa? *)
 227           ##]
 228      ##]
 229   ##]
 230 nqed.
 231
 232 (*
 233 nlemma lift_subst_aux_k: ∀A,B.∀k.
 234   lift_aux (subst_aux B k A) k 1 = subst_aux (lift_aux B k 1) (k+1) A.
 235 #A; #B; nelim B; nnormalize; /2/; #n; #k;
 236 napply (leb_elim (S n) k); nnormalize; #Hnk;
 237   ##[nrewrite > (le_to_leb_true ?? Hnk);
 238      nrewrite > (le_to_leb_true (S n) (k +1) ?);nnormalize;/2/;
 239   ##|nrewrite > (lt_to_leb_false (S (n + 1)) (k+1) ?);
 240     ##[##2: napply le_S_S; napply (monotonic_le_plus_l 1 k n);
 241        napply not_lt_to_le; napply Hnk; ##]
 242     napply (eqb_elim n k);#eqnk;
 243       ##[nrewrite > (eq_to_eqb_true (n+1) (k+1) ?);/2/;
 244          nnormalize; nrewrite < eqnk; //; (* strano *)
 245       ##|nrewrite > (not_eq_to_eqb_false (n+1) (k+1) ?);/2/;
 246          nnormalize;
 247          ncut (O < n);
 248           ##[napply not_le_to_lt;#len;
 249              napply eqnk; napply le_to_le_to_eq;
 250               ##[napply transitive_le; //;
 251               ##|napply not_lt_to_le; /2/;
 252               ##]
 253           ##|#posn;
 254              nrewrite > (lt_to_leb_false (S (n - 1)) k ?);
 255              ##[nnormalize;
 256                 (* nrewrite < (minus_plus_m_m n 1); *)
 257                 nrewrite < (plus_minus_m_m n 1 ?);//;
 258              ##|napply le_S_S; napply not_eq_to_le_to_le_minus;
 259                 ##[/2/;
 260                 ##|napply (not_lt_to_le … Hnk);
 261                 ##]
 262              ##]
 263           ##]
 264        ##]
 265   ##]
 266 nqed.
 267 *)
 268
 269 ntheorem delift : ∀A,B.∀i,j,k. i ≤ j → j ≤ i + k →
 270   subst_aux (lift_aux B i (S k)) j A = (lift_aux B i k).
 271 #A; #B; nelim B; nnormalize; /2/;
 272    ##[##2,3,4: #T; #T0; #Hind1; #Hind2; #i; #j; #k; #leij; #lejk;
 273       napply eq_f2;/2/; napply Hind2;
 274       napplyS (monotonic_le_plus_l 1);//
 275    ##|#n; #i; #j; #k; #leij; #ltjk;
 276       napply (leb_elim (S n) i); nnormalize; #len;
 277       ##[nrewrite > (le_to_leb_true (S n) j ?);/2/;
 278       ##|nrewrite > (lt_to_leb_false (S (n+S k)) j ?);
 279         ##[nnormalize;
 280            nrewrite > (not_eq_to_eqb_false (n+S k) j ?);
 281            nnormalize; /2/; napply (not_to_not …len);
 282            #H; napply (le_plus_to_le_r k); (* why napplyS ltjk; *)
 283            nnormalize; //;
 284         ##|napply le_S_S; napply (transitive_le … ltjk);
 285            napply le_plus;//; napply not_lt_to_le; /2/;
 286         ##]
 287     ##]
 288 nqed.
 289
 290 (********************* substitution lemma ***********************)
 291 nlemma subst_lemma: ∀A,B,C.∀k,i.
 292   subst_aux (subst_aux A i B) (k+i) C =
 293     subst_aux (subst_aux A (S (k+i)) C) i (subst_aux B k C).
 294 #A; #B; #C; #k; nelim A; nnormalize;//; (* WOW *)
 295 #n; #i; napply (leb_elim (S n) i); #Hle;
 296   ##[ncut (n < k+i); ##[/2/##] #ltn; (* lento *)
 297      ncut (n ≤ k+i); ##[/2/##] #len;
 298      nrewrite > (subst_rel1 C (k+i) n ltn);
 299      nrewrite > (le_to_leb_true n (k+i) len);
 300      nrewrite > (subst_rel1 … Hle);//;
 301   ##|napply (eqb_elim n i); #eqni;
 302     ##[nrewrite > eqni;
 303        nrewrite > (le_to_leb_true i (k+i) ?); //;
 304        nrewrite > (subst_rel2 …); nnormalize;
 305        napply symmetric_eq;
 306        napplyS (lift_subst_aux_kij C B i k O);
 307     ##|napply (leb_elim (S (n-1)) (k+i)); #nk;
 308       ##[nrewrite > (subst_rel1 C (k+i) (n-1) nk);
 309          nrewrite > (le_to_leb_true n (k+i) ?);
 310         ##[nrewrite > (subst_rel3 ? i n ?);//;
 311            napply not_eq_to_le_to_lt;
 312             ##[/2/;
 313             ##|napply not_lt_to_le;/2/;
 314             ##]
 315         ##|napply (transitive_le … nk);//;
 316         ##]
 317       ##|ncut (i < n);
 318         ##[napply not_eq_to_le_to_lt; ##[/2/]
 319            napply (not_lt_to_le … Hle);##]
 320          #ltin; ncut (O < n); ##[/2/;##] #posn;
 321          napply (eqb_elim (n-1) (k+i)); #H
 322          ##[nrewrite > H; nrewrite > (subst_rel2 C (k+i));
 323             nrewrite > (lt_to_leb_false n (k+i) ?);
 324             ##[nrewrite > (eq_to_eqb_true n (S(k+i)) ?);
 325               ##[nnormalize;
 326               ##|nrewrite < H; napplyS plus_minus_m_m;//;
 327               ##]
 328             ##|nrewrite < H; napply (lt_O_n_elim … posn);
 329                #m; nnormalize;//;
 330             ##]
 331          ##|ncut (k+i < n-1);
 332             ##[napply not_eq_to_le_to_lt;
 333               ##[napply symmetric_not_eq; napply H;
 334               ##|napply (not_lt_to_le … nk);
 335               ##]
 336             ##]
 337             #Hlt; nrewrite > (lt_to_leb_false n (k+i) ?);
 338             ##[nrewrite > (not_eq_to_eqb_false n (S(k+i)) ?);
 339               ##[nrewrite > (subst_rel3 C (k+i) (n-1) Hlt);
 340                  nrewrite > (subst_rel3 ? i (n-1) ?);//;
 341                  napply (le_to_lt_to_lt … Hlt);//;
 342               ##|napply (not_to_not … H); #Hn; nrewrite > Hn; nnormalize;//;
 343               ##]
 344             ##|napply (transitive_lt … Hlt);
 345                napply (lt_O_n_elim … posn);
 346                #m; nnormalize;//;
 347             ##]
 348           ##]
 349           nrewrite <H;
 350           ncut (∃m:nat. S m = n);
 351           ##[napply (lt_O_n_elim … posn); #m;@ m;//;
 352             ##|*; #m; #Hm; nrewrite < Hm;
 353                nrewrite > (delift ???????);nnormalize;/2/;
 354           ##]
 355 nqed.
 356
 357 (*************************** substl *****************************)
 358
 359 nlet rec substl (G:list T) (N:T) : list T ≝
 360   match G with
 361     [ nil ⇒ nil T
 362     | cons A D ⇒ ((subst_aux A (length T D) N)::(substl D N))
 363     ].
 364
 365
 366 (*****************************************************************)
 367
 368 naxiom A: nat → nat → Prop.
 369 naxiom R: nat → nat → nat → Prop.
 370 naxiom conv: T → T → Prop.
 371
 372 ninductive TJ: list T → T → T → Prop ≝
 373   | ax : ∀i,j. A i j → TJ [] (Sort i) (Sort j)
 374   | start: ∀G.∀A.∀i.TJ G A (Sort i) → TJ (A::G) (Rel 0) (lift A 1)
 375   | weak: ∀G.∀A,B,C.∀i.
 376      TJ G A B → TJ G C (Sort i) → TJ (C::G) (lift A 1) (lift B 1)
 377   | prod: ∀G.∀A,B.∀i,j,k. R i j k →
 378      TJ G A (Sort i) → TJ (A::G) B (Sort j) → TJ G (Prod A B) (Sort k)
 379   | app: ∀G.∀F,A,B,a.
 380      TJ G F (Prod A B) → TJ G a A → TJ G (App F a) (subst B a)
 381   | abs: ∀G.∀A,B,b.∀i.
 382      TJ (A::G) b B → TJ G (Prod A B) (Sort i) → TJ G (Lambda A b) (Prod A B)
 383   | conv: ∀G.∀A,B,C.∀i. conv B C →
 384      TJ G A B → TJ G B (Sort i) → TJ G A C.
 385
 386 ninverter TJ_inv2 for TJ (%?%) : Prop.
 387
 388 (**** definitions ****)
 389
 390 ninductive Glegal (G: list T) : Prop ≝
 391 glegalk : ∀A,B.TJ G A B → Glegal G.
 392
 393 ninductive Gterm (G: list T) (A:T) : Prop ≝
 394   | is_term: ∀B.TJ G A B → Gterm G A
 395   | is_type: ∀B.TJ G B A → Gterm G A.
 396
 397 ninductive Gtype (G: list T) (A:T) : Prop ≝
 398 gtypek: ∀i.TJ G A (Sort i) → Gtype G A.
 399
 400 ninductive Gelement (G:list T) (A:T) : Prop ≝
 401 gelementk: ∀B.TJ G A B → Gtype G B → Gelement G A.
 402
 403 ninductive Tlegal (A:T) : Prop ≝
 404 tlegalk: ∀G. Gterm G A → Tlegal A.
 405
 406 (*
 407 ndefinition Glegal ≝ λG: list T.∃A,B:T.TJ G A B .
 408
 409 ndefinition Gterm ≝ λG: list T.λA.∃B.TJ G A B ∨ TJ G B A.
 410
 411 ndefinition Gtype ≝ λG: list T.λA.∃i.TJ G A (Sort i).
 412
 413 ndefinition Gelement ≝ λG: list T.λA.∃B.TJ G A B ∨ Gtype G B.
 414
 415 ndefinition Tlegal ≝ λA:T.∃G: list T.Gterm G A.
 416 *)
 417
 418 (*
 419 ntheorem free_var1: ∀G.∀A,B,C. TJ G A B →
 420 subst C A
 421 #G; #i; #j; #axij; #Gleg; ncases Gleg;
 422 #A; #B; #tjAB; nelim tjAB; /2/; (* bello *) nqed.
 423 *)
 424
 425 ntheorem start_lemma1: ∀G.∀i,j.
 426 A i j → Glegal G → TJ G (Sort i) (Sort j).
 427 #G; #i; #j; #axij; #Gleg; ncases Gleg;
 428 #A; #B; #tjAB; nelim tjAB; /2/;
 429 (* bello *) nqed.
 430
 431 ntheorem start_rel: ∀G.∀A.∀C.∀n,i,q.
 432 TJ G C (Sort q) → TJ G (Rel n) (lift A i) → TJ (C::G) (Rel (S n)) (lift A (S i)).
 433 #G; #A; #C; #n; #i; #p; #tjC; #tjn;
 434  napplyS (weak G (Rel n));//. (* bello *)
 435  (*
 436  nrewrite > (plus_n_O i);
 437  nrewrite > (plus_n_Sm i O);
 438  nrewrite < (lift_lift A 1 i);
 439  nrewrite > (plus_n_O n);  nrewrite > (plus_n_Sm n O);
 440  applyS (weak G (Rel n) (lift A i) C p tjn tjC). *)
 441 nqed.
 442
 443 ntheorem start_lemma2: ∀G.
 444 Glegal G → ∀n. n < length T G → TJ G (Rel n) (lift (nth n T G (Rel O)) (S n)).
 445 #G; #Gleg; ncases Gleg; #A; #B; #tjAB; nelim tjAB; /2/;
 446   ##[#i; #j; #axij; #p; nnormalize; #abs; napply False_ind;
 447      napply (absurd … abs); //;
 448   ##|#G; #A; #i; #tjA; #Hind; #m; ncases m; /2/;
 449      #p; #Hle; napply start_rel; //; napply Hind;
 450      napply le_S_S_to_le; napply Hle;
 451   ##|#G; #A; #B; #C; #i; #tjAB; #tjC; #Hind1; #_; #m; ncases m;
 452      /2/; #p; #Hle; napply start_rel; //;
 453      napply Hind1; napply le_S_S_to_le; napply Hle;
 454   ##]
 455 nqed.
 456
 457 (*
 458 nlet rec TJm G D on D : Prop ≝
 459   match D with
 460     [ nil ⇒ True
 461     | cons A D1 ⇒ TJ G (Rel 0) A ∧ TJm G D1
 462     ].
 463
 464 nlemma tjm1: ∀G,D.∀A. TJm G (A::D) → TJ G (Rel 0) A.
 465 #G; #D; #A; *; //; nqed.
 466
 467 ntheorem transitivity_tj: ∀D.∀A,B. TJ D A B →
 468   ∀G. Glegal G → TJm G D → TJ G A B.
 469 #D; #A; #B; #tjAB; nelim tjAB;
 470   ##[/2/;
 471   ##|/2/;
 472   ##|#E; #T; #T0; #T1; #n; #tjT; #tjT1; #H; #H1; #G; #HlegG;
 473      #tjGcons;
 474      napply weak;
 475 *)
 476 (*
 477 ntheorem substitution_tj:
 478 ∀G.∀A,B,N,M.TJ (A::G) M B → TJ G N A →
 479   TJ G (subst N M) (subst N B).
 480 #G;#A;#B;#N;#M;#tjM;
 481   napply (TJ_inv2 (A::G) M B);
 482   ##[nnormalize; /3/;
 483   ##|#G; #A; #N; #tjA; #Hind; #Heq;
 484      ndestruct;//;
 485   ##|#G; #A; #B; #C; #n; #tjA; #tjC; #Hind1; #Hind2; #Heq;
 486      ndestruct;//;
 487   ##|nnormalize; #E; #A; #B; #i; #j; #k;
 488      #Ax; #tjA; #tjB; #Hind1; #_;
 489      #Heq; #HeqB; #tjN; napply (prod ?????? Ax);
 490       ##[/2/;
 491       ##|nnormalize; napplyS weak;
 492
 493 *)
 494
 495 ntheorem substitution_tj:
 496 ∀E.∀A,B,M.TJ E M B → ∀G,D.∀N. E = D@A::G → TJ G N A →
 497   TJ ((substl D N)@G) (subst_aux M (length ? D) N) (subst_aux B (length ? D) N).
 498 #E; #A; #B; #M; #tjMB; nelim tjMB;
 499   ##[nnormalize; #i; #j; #k; #G; #D; #N; ncases D;
 500       ##[nnormalize; #isnil; ndestruct;
 501       ##|#P; #L; nnormalize; #isnil; ndestruct;
 502       ##]
 503   ##|#G; #A1; #i; #tjA; #Hind; #G1; #D; ncases D;
 504     ##[#N; #Heq; #tjN;
 505        nrewrite > (delift (lift N O) A1 O O O ??); //;
 506        nnormalize in Heq; ndestruct;/2/;
 507     ##|#H; #L; #N1; #Heq; nnormalize in Heq;
 508        #tjN1; nnormalize; ndestruct;
 509        (* porcherie *)
 510        ncut (S (length T L) = S ((length T L)+0)); ##[//##] #Heq;
 511        nrewrite > Heq;
 512        nrewrite < (lift_subst_aux_k N1 H (length T L) O);
 513        nrewrite < (plus_n_O (length T L));
 514        napply start;/2/;
 515     ##]
 516   ##|#G; #P; #Q; #R; #i; #tjP; #tjR; #Hind1; #Hind2;
 517      #G1; #D; #N; ncases D; nnormalize;
 518     ##[#Heq; ndestruct; #tjN; //;
 519     ##|#H; #L; #Heq;
 520        #tjN1; ndestruct;
 521        (* porcherie *)
 522        ncut (S (length T L) = S ((length T L)+0)); ##[//##] #Heq;
 523        nrewrite > Heq;
 524        nrewrite < (lift_subst_aux_k N P (length T L) O);
 525        nrewrite < (lift_subst_aux_k N Q (length T L) O);
 526        nrewrite < (plus_n_O (length T L));
 527        napply weak;/2/;
 528     ##]
 529   ##|#G; #P; #Q; #i; #j; #k; #Ax; #tjP; #tjQ; #Hind1; #Hind2;
 530      #G1; #D; #N; #Heq; #tjN;
 531      napply (prod … Ax);
 532     ##[/2/;
 533     ##|
 534     ##]
 535   ##|#G; #P; #Q; #R; #S; #tjP; #tjS; #Hind1; #Hind2;
 536      #G1; #D; #N; #Heq; #tjN; nnormalize;
 537      ncheck app.
 538
 539
 540
 541
 542 ntheorem substitution_tj:
 543 ∀E.∀A,B,M.TJ E M B → ∀G,D.∀N. E = D@A::G → TJ G N A →
 544 ∀k.length ? D = k →
 545   TJ ((substl D N)@G) (subst_aux M k N) (subst_aux B k N).
 546 #E; #A; #B; #M; #tjMB; nelim tjMB;
 547   ##[nnormalize; (* /3/; *)
 548   ##|#G; #A1; #i; #tjA; #Hind;
 549      #G1; #D; ncases D;
 550     ##[#N; #Heq; #tjN; #k; nnormalize in ⊢ (% → ?); #kO;
 551        nrewrite < kO;
 552        nrewrite > (delift (lift N O) A1 O O O ??); //;
 553        nnormalize in Heq; ndestruct;/2/;
 554     ##|#H; #L; #N1; #Heq; nnormalize in Heq;
 555        #tjN1; #k; #len; nnormalize in len;
 556        nrewrite < len;
 557        nnormalize; ndestruct;
 558        (* porcherie *)
 559        ncut (S (length T L) = S ((length T L)+0)); ##[//##] #Heq;
 560        nrewrite > Heq;
 561        nrewrite < (lift_subst_aux_k N1 H (length T L) O);
 562        nrewrite < (plus_n_O (length T L));
 563        napply (start (substl L N1@G1) (subst_aux H (length T L) N1) i ?).
 564        napply Hind;//;
 565     ##]
 566
 567
 568
 569
 570
 571
 572
 573