- (∀I,G,K,V. ⦃G,K⦄ ⊢ V![a,h] → Q G K V → Q G (K.ⓑ{I}V) (#O)) →
- (∀I,G,K,i. ⦃G,K⦄ ⊢ #i![a,h] → Q G K (#i) → Q G (K.ⓘ{I}) (#(↑i))) →
- (∀p,I,G,L,V,T. ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L.ⓑ{I}V⦄⊢T![a,h] →
+ (∀I,G,K,V. ⦃G,K⦄ ⊢ V![h,a] → Q G K V → Q G (K.ⓑ{I}V) (#O)) →
+ (∀I,G,K,i. ⦃G,K⦄ ⊢ #i![h,a] → Q G K (#i) → Q G (K.ⓘ{I}) (#(↑i))) →
+ (∀p,I,G,L,V,T. ⦃G,L⦄ ⊢ V![h,a] → ⦃G,L.ⓑ{I}V⦄⊢T![h,a] →