(* Properties with normal terms for unbound parallel rt-transition **********)
(* Basic_1: was just: sn3_appls_lref *)
-lemma csx_applv_cnx: ∀h,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ →
- ∀Vs. ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃Vs⦄ → ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.T⦄.
+lemma csx_applv_cnx: ∀h,G,L,T. 𝐒⦃T⦄ → ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ →
+ ∀Vs. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃Vs⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.T⦄.
#h #G #L #T #H1T #H2T #Vs elim Vs -Vs
[ #_ normalize in ⊢ (????%); /2 width=1 by cnx_csx/
| #V #Vs #IHV #H
(* Advanced properties ******************************************************)
-lemma csx_applv_sort: ∀h,G,L,s,Vs. ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃Vs⦄ → ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.⋆s⦄.
+lemma csx_applv_sort: ∀h,G,L,s,Vs. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃Vs⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃ⒶVs.⋆s⦄.
/3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ qed.