- ∀L,i. G ⊢ ⬈*[h,#i] 𝐒⦃L⦄ →
- â\88¨â\88¨ â\87©*[â\92»,ð\9d\90\94â\9d´iâ\9dµ] L ≘ ⋆
- | ∃∃I,K. ⇩*[i] L ≘ K.ⓤ{I}
- | ∃∃I,K,V. ⇩*[i] L ≘ K.ⓑ{I}V & ⦃G,K⦄ ⊢ ⬈*[h] 𝐒⦃V⦄ & G ⊢ ⬈*[h,V] 𝐒⦃K⦄.
+ ∀L,i. G ⊢ ⬈*𝐒[h,#i] L →
+ â\88¨â\88¨ â\87©*[â\92»,ð\9d\90\94â\9d¨iâ\9d©] L ≘ ⋆
+ | ∃∃I,K. ⇩[i] L ≘ K.ⓤ[I]
+ | ∃∃I,K,V. ⇩[i] L ≘ K.ⓑ[I]V & ❪G,K❫ ⊢ ⬈*𝐒[h] V & G ⊢ ⬈*𝐒[h,V] K.