- | ⦃G1, L1, V1⦄ ⊐*[b] ⦃G2, L2, T2⦄
- | ⦃G1, L1.ⓑ{I}V1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄
- | ⦃G1, L1.ⓧ, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ ∧ b = Ⓕ
- | ∃∃J,L,T. ⦃G1, L, T⦄ ⊐*[b] ⦃G2, L2, T2⦄ & ⬆*[1] T ≘ ⓑ{p,I}V1.T1 & L1 = L.ⓘ{J}.
+ | ⦃G1,L1,V1⦄ ⊐*[b] ⦃G2,L2,T2⦄
+ | ⦃G1,L1.ⓑ{I}V1,T1⦄ ⊐*[b] ⦃G2,L2,T2⦄
+ | ⦃G1,L1.ⓧ,T1⦄ ⊐*[b] ⦃G2,L2,T2⦄ ∧ b = Ⓕ
+ | ∃∃J,L,T. ⦃G1,L,T⦄ ⊐*[b] ⦃G2,L2,T2⦄ & ⬆*[1] T ≘ ⓑ{p,I}V1.T1 & L1 = L.ⓘ{J}.