- â\88\80X. â¦\83G,Lâ¦\84 ⊢ ⓐV.T :[h,a] X →
- â\88¨â\88¨ â\88\83â\88\83p,W,U,U0. ad a 0 & â¦\83G,Lâ¦\84 â\8a¢ V :[h,a] W & â¦\83G,Lâ¦\84 â\8a¢ T :*[h,a,0] â\93\9b{p}W.U0 & â¦\83G,L.â\93\9bWâ¦\84 â\8a¢ U0 :[h,a] U & â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.â\93\9b{p}W.U â¬\8c*[h] X & â¦\83G,Lâ¦\84 ⊢ X ![h,a]
- | â\88\83â\88\83n,p,W,U,U0. ad a (â\86\91n) & â¦\83G,Lâ¦\84 â\8a¢ V :[h,a] W & â¦\83G,Lâ¦\84 â\8a¢ T :[h,a] U & â¦\83G,Lâ¦\84 â\8a¢ U :*[h,a,n] â\93\9b{p}W.U0 & â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.U â¬\8c*[h] X & â¦\83G,Lâ¦\84 ⊢ X ![h,a].
+ â\88\80X. â\9dªG,Lâ\9d« ⊢ ⓐV.T :[h,a] X →
+ â\88¨â\88¨ â\88\83â\88\83p,W,U,U0. ad a 0 & â\9dªG,Lâ\9d« â\8a¢ V :[h,a] W & â\9dªG,Lâ\9d« â\8a¢ T :*[h,a,0] â\93\9b[p]W.U0 & â\9dªG,L.â\93\9bWâ\9d« â\8a¢ U0 :[h,a] U & â\9dªG,Lâ\9d« â\8a¢ â\93\90V.â\93\9b[p]W.U â¬\8c*[h] X & â\9dªG,Lâ\9d« ⊢ X ![h,a]
+ | â\88\83â\88\83n,p,W,U,U0. ad a (â\86\91n) & â\9dªG,Lâ\9d« â\8a¢ V :[h,a] W & â\9dªG,Lâ\9d« â\8a¢ T :[h,a] U & â\9dªG,Lâ\9d« â\8a¢ U :*[h,a,n] â\93\9b[p]W.U0 & â\9dªG,Lâ\9d« â\8a¢ â\93\90V.U â¬\8c*[h] X & â\9dªG,Lâ\9d« ⊢ X ![h,a].