- â\88\80I,K,V1,V2,i. â\87©[i] L â\89\98 K.â\93\91[I]V1 â\86\92 â\9dªG,Kâ\9d« ⊢ V1 ⬈* V2 →
- â\88\80W2. â\87§[â\86\91i] V2 â\89\98 W2 â\86\92 â\9dªG,Lâ\9d« ⊢ #i ⬈* W2.
+ â\88\80I,K,V1,V2,i. â\87©[i] L â\89\98 K.â\93\91[I]V1 â\86\92 â\9d¨G,Kâ\9d© ⊢ V1 ⬈* V2 →
+ â\88\80W2. â\87§[â\86\91i] V2 â\89\98 W2 â\86\92 â\9d¨G,Lâ\9d© ⊢ #i ⬈* W2.