- â\88\80U1,T1. â\9dªG,Lâ\9d« ⊢ ⓝU1.T1 ![h,a] →
- â\88\80X. â\9dªG,Lâ\9d« â\8a¢ â\93\9dU1.T1 â\9e¡[h,n] X â\86\92 â\93\9dU1.T1 â\89\9b X →
- â\88\83â\88\83U0,U2,T2. â\9dªG,Lâ\9d« â\8a¢ U1 â\9e¡*[h,0] U0 & â\9dªG,Lâ\9d« ⊢ T1 ➡*[h,1] U0
- & â\9dªG,Lâ\9d« â\8a¢ U1 ![h,a] & â\9dªG,Lâ\9d« â\8a¢ U1 â\9e¡[h,n] U2 & U1 â\89\9b U2
- & â\9dªG,Lâ\9d« â\8a¢ T1 ![h,a] & â\9dªG,Lâ\9d« â\8a¢ T1 â\9e¡[h,n] T2 & T1 â\89\9b T2 & X = ⓝU2.T2.
+ â\88\80U1,T1. â\9d¨G,Lâ\9d© ⊢ ⓝU1.T1 ![h,a] →
+ â\88\80X. â\9d¨G,Lâ\9d© â\8a¢ â\93\9dU1.T1 â\9e¡[h,n] X â\86\92 â\93\9dU1.T1 â\89\85 X →
+ â\88\83â\88\83U0,U2,T2. â\9d¨G,Lâ\9d© â\8a¢ U1 â\9e¡*[h,0] U0 & â\9d¨G,Lâ\9d© ⊢ T1 ➡*[h,1] U0
+ & â\9d¨G,Lâ\9d© â\8a¢ U1 ![h,a] & â\9d¨G,Lâ\9d© â\8a¢ U1 â\9e¡[h,n] U2 & U1 â\89\85 U2
+ & â\9d¨G,Lâ\9d© â\8a¢ T1 ![h,a] & â\9d¨G,Lâ\9d© â\8a¢ T1 â\9e¡[h,n] T2 & T1 â\89\85 T2 & X = ⓝU2.T2.