- (â\88\80I,G,K,V. â¦\83G,Kâ¦\84 â\8a¢ V![h,a] â\86\92 Q G K V â\86\92 Q G (K.â\93\91{I}V) (#O)) →
- (â\88\80I,G,K,i. â¦\83G,Kâ¦\84 â\8a¢ #i![h,a] â\86\92 Q G K (#i) â\86\92 Q G (K.â\93\98{I}) (#(↑i))) →
- (â\88\80p,I,G,L,V,T. â¦\83G,Lâ¦\84 â\8a¢ V![h,a] â\86\92 â¦\83G,L.â\93\91{I}Vâ¦\84⊢T![h,a] →
- Q G L V →Q G (L.ⓑ{I}V) T →Q G L (ⓑ{p,I}V.T)
+ (â\88\80I,G,K,V. â\9dªG,Kâ\9d« â\8a¢ V![h,a] â\86\92 Q G K V â\86\92 Q G (K.â\93\91[I]V) (#O)) →
+ (â\88\80I,G,K,i. â\9dªG,Kâ\9d« â\8a¢ #i![h,a] â\86\92 Q G K (#i) â\86\92 Q G (K.â\93\98[I]) (#(↑i))) →
+ (â\88\80p,I,G,L,V,T. â\9dªG,Lâ\9d« â\8a¢ V![h,a] â\86\92 â\9dªG,L.â\93\91[I]Vâ\9d«⊢T![h,a] →
+ Q G L V →Q G (L.ⓑ[I]V) T →Q G L (ⓑ[p,I]V.T)