- (∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → Q G2 L2 T2) →
- (∀G,G2,L,L2,T,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G, L, T⦄ → ⦃G, L, T⦄ ⊐[b] ⦃G2, L2, T2⦄ → Q G L T → Q G2 L2 T2) →
- ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → Q G2 L2 T2.
+ (∀G2,L2,T2. ⦃G1,L1,T1⦄ ⊐[b] ⦃G2,L2,T2⦄ → Q G2 L2 T2) →
+ (∀G,G2,L,L2,T,T2. ⦃G1,L1,T1⦄ ⊐+[b] ⦃G,L,T⦄ → ⦃G,L,T⦄ ⊐[b] ⦃G2,L2,T2⦄ → Q G L T → Q G2 L2 T2) →
+ ∀G2,L2,T2. ⦃G1,L1,T1⦄ ⊐+[b] ⦃G2,L2,T2⦄ → Q G2 L2 T2.