- (∀G,L,s. Q G L (⋆s) (⋆(next h s))) →
- (∀I,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 → Q G K V1 V2 →
- â¬\86*[1] V2 ≘ W2 → Q G (K.ⓑ{I}V1) (#0) W2
- ) → (∀I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ⬈[h] T → Q G K (#i) T →
- â¬\86*[1] T ≘ U → Q G (K.ⓘ{I}) (#↑i) (U)
- ) → (∀p,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[h] T2 →
+ (∀G,L,s. Q G L (⋆s) (⋆(⫯[h]s))) →
+ (∀I,G,K,V1,V2,W2. ⦃G,K⦄ ⊢ V1 ⬈[h] V2 → Q G K V1 V2 →
+ â\87§*[1] V2 ≘ W2 → Q G (K.ⓑ{I}V1) (#0) W2
+ ) → (∀I,G,K,T,U,i. ⦃G,K⦄ ⊢ #i ⬈[h] T → Q G K (#i) T →
+ â\87§*[1] T ≘ U → Q G (K.ⓘ{I}) (#↑i) (U)
+ ) → (∀p,I,G,L,V1,V2,T1,T2. ⦃G,L⦄ ⊢ V1 ⬈[h] V2 → ⦃G,L.ⓑ{I}V1⦄ ⊢ T1 ⬈[h] T2 →