(**************************************************************************)
include "basic_2/notation/relations/sn_6.ma".
-include "basic_2/substitution/lleq.ma".
+include "basic_2/multiple/lleq.ma".
include "basic_2/reduction/lpx.ma".
(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
lemma lsx_ind: ∀h,g,G,T,d. ∀R:predicate lenv.
(∀L1. G ⊢ ⬊*[h, g, T, d] L1 →
- (â\88\80L2. â¦\83G, L1â¦\84 â\8a¢ â\9e¡[h, g] L2 â\86\92 (L1 â\8b\95[T, d] L2 → ⊥) → R L2) →
+ (â\88\80L2. â¦\83G, L1â¦\84 â\8a¢ â\9e¡[h, g] L2 â\86\92 (L1 â\89¡[T, d] L2 → ⊥) → R L2) →
R L1
) →
∀L. G ⊢ ⬊*[h, g, T, d] L → R L.
(* Basic properties *********************************************************)
lemma lsx_intro: ∀h,g,G,L1,T,d.
- (â\88\80L2. â¦\83G, L1â¦\84 â\8a¢ â\9e¡[h, g] L2 â\86\92 (L1 â\8b\95[T, d] L2 → ⊥) → G ⊢ ⬊*[h, g, T, d] L2) →
+ (â\88\80L2. â¦\83G, L1â¦\84 â\8a¢ â\9e¡[h, g] L2 â\86\92 (L1 â\89¡[T, d] L2 → ⊥) → G ⊢ ⬊*[h, g, T, d] L2) →
G ⊢ ⬊*[h, g, T, d] L1.
/5 width=1 by lleq_sym, SN_intro/ qed.
qed.
lemma lsx_ge_up: ∀h,g,G,L,T,U,dt,d,e. dt ≤ yinj d + yinj e →
- â\87§[d, e] T ≡ U → G ⊢ ⬊*[h, g, U, dt] L → G ⊢ ⬊*[h, g, U, d] L.
+ â¬\86[d, e] T ≡ U → G ⊢ ⬊*[h, g, U, dt] L → G ⊢ ⬊*[h, g, U, d] L.
#h #g #G #L #T #U #dt #d #e #Hdtde #HTU #H @(lsx_ind … H) -L
/5 width=7 by lsx_intro, lleq_ge_up/
qed-.