(* Properties with evaluation for t-bound rt-transition on terms ************)
+lemma cnv_cpme_trans (a) (h) (n) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
+ ∀T2. ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T2 ![a,h].
+#a #h #n #G #L #T1 #HT1 #T2 * #HT12 #_
+/2 width=4 by cnv_cpms_trans/
+qed-.
+
lemma cnv_cpme_cpms_conf (a) (h) (n) (G) (L):
∀T. ⦃G,L⦄ ⊢ T ![a,h] → ∀T1. ⦃G,L⦄ ⊢ T ➡*[n,h] T1 →
∀T2. ⦃G,L⦄ ⊢ T ➡*[h,n] 𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T1 ➡*[h] 𝐍⦃T2⦄.