- â\88\80W1,T1,X2. â\9dªG,Lâ\9d« ⊢ ⓝW1.T1 ➡*[h,n] X2 →
- â\88¨â\88¨ â\88\83â\88\83W2,T2. â\9dªG,Lâ\9d« â\8a¢ W1 â\9e¡*[h,n] W2 & â\9dªG,Lâ\9d« ⊢ T1 ➡*[h,n] T2 & X2 = ⓝW2.T2
- | â\9dªG,Lâ\9d« ⊢ T1 ➡*[h,n] X2
- | â\88\83â\88\83m. â\9dªG,Lâ\9d« ⊢ W1 ➡*[h,m] X2 & n = ↑m.
+ â\88\80W1,T1,X2. â\9d¨G,Lâ\9d© ⊢ ⓝW1.T1 ➡*[h,n] X2 →
+ â\88¨â\88¨ â\88\83â\88\83W2,T2. â\9d¨G,Lâ\9d© â\8a¢ W1 â\9e¡*[h,n] W2 & â\9d¨G,Lâ\9d© ⊢ T1 ➡*[h,n] T2 & X2 = ⓝW2.T2
+ | â\9d¨G,Lâ\9d© ⊢ T1 ➡*[h,n] X2
+ | â\88\83â\88\83m. â\9d¨G,Lâ\9d© ⊢ W1 ➡*[h,m] X2 & n = ↑m.