- â\88\80A. â\9dªG,Lâ\9d« ⊢ T ⁝ A →
- â\88\80n1,U1. â\9dªG,Lâ\9d« ⊢ T ➡*[h,n1] ⓛ[p]W.U1 → ∀n2. n1 ≤ n2 →
- â\88\83â\88\83U2. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[h,n2] â\93\9b[p]W.U2 & â\9dªG,L.â\93\9bWâ\9d« ⊢ U1 ➡*[h,n2-n1] U2.
+ â\88\80A. â\9d¨G,Lâ\9d© ⊢ T ⁝ A →
+ â\88\80n1,U1. â\9d¨G,Lâ\9d© ⊢ T ➡*[h,n1] ⓛ[p]W.U1 → ∀n2. n1 ≤ n2 →
+ â\88\83â\88\83U2. â\9d¨G,Lâ\9d© â\8a¢ T â\9e¡*[h,n2] â\93\9b[p]W.U2 & â\9d¨G,L.â\93\9bWâ\9d© ⊢ U1 ➡*[h,n2-n1] U2.