| lcosx_sort: ∀l. lcosx h g G l (⋆)
| lcosx_skip: ∀I,L,T. lcosx h g G 0 L → lcosx h g G 0 (L.ⓑ{I}T)
| lcosx_pair: ∀I,L,T,l. G ⊢ ⬊*[h, g, T, l] L →
| lcosx_sort: ∀l. lcosx h g G l (⋆)
| lcosx_skip: ∀I,L,T. lcosx h g G 0 L → lcosx h g G 0 (L.ⓑ{I}T)
| lcosx_pair: ∀I,L,T,l. G ⊢ ⬊*[h, g, T, l] L →