-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 #_
+lemma cnv_cpme_trans (h) (a) (n) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![h,a] →
+ ∀T2. ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T2 ![h,a].
+#h #a #n #G #L #T1 #HT1 #T2 * #HT12 #_