-lemma nta_cpcs_conf (a) (h) (G) (L):
- ∀T1,U. ⦃G,L⦄ ⊢ T1 :[a,h] U → ∀T2. ⦃G,L⦄ ⊢ T1 ⬌*[h] T2 →
- ∀U0. ⦃G,L⦄ ⊢ T2 :[a,h] U0 → ⦃G,L⦄ ⊢ T2 :[a,h] U.
-#a #h #G #L #T1 #U #HT1 #T2 #HT12 #U0 #HT2
+lemma nta_cpcs_conf (h) (a) (G) (L):
+ ∀T1,U. ⦃G,L⦄ ⊢ T1 :[h,a] U → ∀T2. ⦃G,L⦄ ⊢ T1 ⬌*[h] T2 →
+ ∀U0. ⦃G,L⦄ ⊢ T2 :[h,a] U0 → ⦃G,L⦄ ⊢ T2 :[h,a] U.
+#h #a #G #L #T1 #U #HT1 #T2 #HT12 #U0 #HT2