- â\88\80V,W. â¦\83G,Lâ¦\84 ⊢ V :[h,a] W →
- â\88\80T,U. â¦\83G,L.â\93\9bWâ¦\84 â\8a¢ T :[h,a] U â\86\92 â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.â\93\9b{p}W.T :[h,a] â\93\90V.â\93\9b{p}W.U.
+ â\88\80V,W. â\9dªG,Lâ\9d« ⊢ V :[h,a] W →
+ â\88\80T,U. â\9dªG,L.â\93\9bWâ\9d« â\8a¢ T :[h,a] U â\86\92 â\9dªG,Lâ\9d« â\8a¢ â\93\90V.â\93\9b[p]W.T :[h,a] â\93\90V.â\93\9b[p]W.U.