- â\88\80p,I,L1,V. G â\8a¢ â¬\88*[h,V] ð\9d\90\92â¦\83L1â¦\84 →
- â\88\80Y,T. G â\8a¢ â¬\88*[h,T] ð\9d\90\92â¦\83Yâ¦\84 →
- â\88\80L2. Y = L2.â\93§ â\86\92 â¦\83G,L1â¦\84 ⊢ ⬈*[h] L2 →
- G ⊢ ⬈*[h,ⓑ{p,I}V.T] 𝐒⦃L2⦄.
+ â\88\80p,I,L1,V. G â\8a¢ â¬\88*[h,V] ð\9d\90\92â\9dªL1â\9d« →
+ â\88\80Y,T. G â\8a¢ â¬\88*[h,T] ð\9d\90\92â\9dªYâ\9d« →
+ â\88\80L2. Y = L2.â\93§ â\86\92 â\9dªG,L1â\9d« ⊢ ⬈*[h] L2 →
+ G ⊢ ⬈*[h,ⓑ[p,I]V.T] 𝐒❪L2❫.