-
-
-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;//;
- ##]
-
-
-