∀T1,T0. ⦃G,L⦄ ⊢T1 ➡*[n,h] T0 →
∀T2. ⦃G,L⦄ ⊢ T0 ➡*[h] 𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍⦃T2⦄.
#h #n #G #L #T1 #T0 #HT10 #T2 * #HT02 #HT2
∀T1,T0. ⦃G,L⦄ ⊢T1 ➡*[n,h] T0 →
∀T2. ⦃G,L⦄ ⊢ T0 ➡*[h] 𝐍⦃T2⦄ → ⦃G,L⦄ ⊢ T1 ➡*[h,n] 𝐍⦃T2⦄.
#h #n #G #L #T1 #T0 #HT10 #T2 * #HT02 #HT2