-(*
-nlet rec TJm G D on D : Prop ≝
- match D with
- [ nil ⇒ True
- | cons A D1 ⇒ TJ G (Rel 0) A ∧ TJm G D1
- ].
-
-nlemma tjm1: ∀G,D.∀A. TJm G (A::D) → TJ G (Rel 0) A.
-#G; #D; #A; *; //; nqed.
-
-ntheorem transitivity_tj: ∀D.∀A,B. TJ D A B →
- ∀G. Glegal G → TJm G D → TJ G A B.
-#D; #A; #B; #tjAB; nelim tjAB;
- ##[/2/;
- ##|/2/;
- ##|#E; #T; #T0; #T1; #n; #tjT; #tjT1; #H; #H1; #G; #HlegG;
- #tjGcons;
- napply weak;
-*)
-(*
-ntheorem substitution_tj:
-∀G.∀A,B,N,M.TJ (A::G) M B → TJ G N A →
- TJ G (subst N M) (subst N B).
-#G;#A;#B;#N;#M;#tjM;
- napply (TJ_inv2 (A::G) M B);
- ##[nnormalize; /3/;
- ##|#G; #A; #N; #tjA; #Hind; #Heq;
- ndestruct;//;
- ##|#G; #A; #B; #C; #n; #tjA; #tjC; #Hind1; #Hind2; #Heq;
- ndestruct;//;
- ##|nnormalize; #E; #A; #B; #i; #j; #k;
- #Ax; #tjA; #tjB; #Hind1; #_;
- #Heq; #HeqB; #tjN; napply (prod ?????? Ax);
- ##[/2/;
- ##|nnormalize; napplyS weak;
-
-*)
-
-
-axiom conv_subst: ∀P,Q,N,i.conv P Q → conv P[i := N] Q[i := N].