+(* EXTENDED CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS *************)
+
+(* Properties with normal forms *********************************************)
+
+lemma cpxs_cnx (G) (L) (T1):
+ (∀T2. ❨G,L❩ ⊢ T1 ⬈* T2 → T1 ≅ T2) → ❨G,L❩ ⊢ ⬈𝐍 T1.
+/3 width=1 by cpx_cpxs/ qed.