- â\88\80V1. â\9dªG0,L0â\9d« ⊢ V0 ➡[h,0] V1 → ∀U1. ⇧[1] V1 ≘ U1 →
- â\88\80W1. â\9dªG0,L0â\9d« â\8a¢ W0 â\9e¡[h,0] W1 â\86\92 â\88\80T1. â\9dªG0,L0.â\93\93W0â\9d« ⊢ T0 ➡[h,0] T1 →
- â\88\80V2. â\9dªG0,L0â\9d« ⊢ V0 ➡[h,0] V2 → ∀U2. ⇧[1] V2 ≘ U2 →
- â\88\80W2. â\9dªG0,L0â\9d« â\8a¢ W0 â\9e¡[h,0] W2 â\86\92 â\88\80T2. â\9dªG0,L0.â\93\93W0â\9d« ⊢ T0 ➡[h,0] T2 →
- â\88\80L1. â\9dªG0,L0â\9d« â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9dªG0,L0â\9d« ⊢ ➡[h,0] L2 →
- â\88\83â\88\83T. â\9dªG0,L1â\9d« â\8a¢ â\93\93[p]W1.â\93\90U1.T1 â\9e¡[h,0] T & â\9dªG0,L2â\9d« ⊢ ⓓ[p]W2.ⓐU2.T2 ➡[h,0] T.
+ â\88\80V1. â\9d¨G0,L0â\9d© ⊢ V0 ➡[h,0] V1 → ∀U1. ⇧[1] V1 ≘ U1 →
+ â\88\80W1. â\9d¨G0,L0â\9d© â\8a¢ W0 â\9e¡[h,0] W1 â\86\92 â\88\80T1. â\9d¨G0,L0.â\93\93W0â\9d© ⊢ T0 ➡[h,0] T1 →
+ â\88\80V2. â\9d¨G0,L0â\9d© ⊢ V0 ➡[h,0] V2 → ∀U2. ⇧[1] V2 ≘ U2 →
+ â\88\80W2. â\9d¨G0,L0â\9d© â\8a¢ W0 â\9e¡[h,0] W2 â\86\92 â\88\80T2. â\9d¨G0,L0.â\93\93W0â\9d© ⊢ T0 ➡[h,0] T2 →
+ â\88\80L1. â\9d¨G0,L0â\9d© â\8a¢ â\9e¡[h,0] L1 â\86\92 â\88\80L2. â\9d¨G0,L0â\9d© ⊢ ➡[h,0] L2 →
+ â\88\83â\88\83T. â\9d¨G0,L1â\9d© â\8a¢ â\93\93[p]W1.â\93\90U1.T1 â\9e¡[h,0] T & â\9d¨G0,L2â\9d© ⊢ ⓓ[p]W2.ⓐU2.T2 ➡[h,0] T.