- â\88\80Vs,W,T,X2. â\9dªG,Lâ\9d« ⊢ ⒶVs.ⓝW.T ⬈* X2 →
- ∨∨ ⒶVs. ⓝW. T ⩳ X2
- | â\9dªG,Lâ\9d« ⊢ ⒶVs.T ⬈* X2
- | â\9dªG,Lâ\9d« ⊢ ⒶVs.W ⬈* X2.
+ â\88\80Vs,W,T,X2. â\9d¨G,Lâ\9d© ⊢ ⒶVs.ⓝW.T ⬈* X2 →
+ ∨∨ ⒶVs. ⓝW. T ~ X2
+ | â\9d¨G,Lâ\9d© ⊢ ⒶVs.T ⬈* X2
+ | â\9d¨G,Lâ\9d© ⊢ ⒶVs.W ⬈* X2.