- ∀I,K1,L2. G ⊢ K1.ⓘ{I} ⊒[h] L2 →
- ∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & L2 = K2.ⓘ{I}
- | â\88\83â\88\83J,K2,V. G â\8a¢ K1 â\8a\92[h] K2 & G â\8a¢ â¬\88*[h,V] ð\9d\90\92â¦\83K2â¦\84 & I = BPair J V & L2 = K2.ⓧ.
+ ∀I,K1,L2. G ⊢ K1.ⓘ[I] ⊒[h] L2 →
+ ∨∨ ∃∃K2. G ⊢ K1 ⊒[h] K2 & L2 = K2.ⓘ[I]
+ | â\88\83â\88\83J,K2,V. G â\8a¢ K1 â\8a\92[h] K2 & G â\8a¢ â¬\88*[h,V] ð\9d\90\92â\9dªK2â\9d« & I = BPair J V & L2 = K2.ⓧ.