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