- ∀I,K1,L2. G ⊢ K1.ⓘ{I} ⊒[h] L2 →
- ∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & L2 = K2.ⓘ{I}
- | ∃∃J,K2,V. G ⊢ K1 ⊒[h] K2 & G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ & I = BPair J V & L2 = K2.ⓧ.
+ ∀I,K1,L2. G ⊢ K1.ⓘ[I] ⊒[h] L2 →
+ ∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & L2 = K2.ⓘ[I]
+ | ∃∃J,K2,V. G ⊢ K1 ⊒[h] K2 & G ⊢ ⬈*𝐒[h,V] K2 & I = BPair J V & L2 = K2.ⓧ.