(* 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.