(* Properties with normal terms for unbound parallel rt-transition **********)
(* Basic_1: was just: sn3_nf2 *)
-lemma cnx_csx: ∀h,G,L,T. ⦃G, L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ → ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃T⦄.
+lemma cnx_csx: ∀h,G,L,T. ⦃G,L⦄ ⊢ ⬈[h] 𝐍⦃T⦄ → ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃T⦄.
/2 width=1 by NF_to_SN/ qed.
(* Advanced properties ******************************************************)
-lemma csx_sort: ∀h,G,L,s. ⦃G, L⦄ ⊢ ⬈*[h] 𝐒⦃⋆s⦄.
+lemma csx_sort: ∀h,G,L,s. ⦃G,L⦄ ⊢ ⬈*[h] 𝐒⦃⋆s⦄.
/3 width=4 by cnx_csx, cnx_sort/ qed.