| cpx_atom : ∀I,G,L. cpx h g G L (⓪{I}) (⓪{I})
| cpx_sort : ∀G,L,k,l. deg h g k (l+1) → cpx h g G L (⋆k) (⋆(next h k))
| cpx_delta: ∀I,G,L,K,V,V2,W2,i.
| cpx_atom : ∀I,G,L. cpx h g G L (⓪{I}) (⓪{I})
| cpx_sort : ∀G,L,k,l. deg h g k (l+1) → cpx h g G L (⋆k) (⋆(next h k))
| cpx_delta: ∀I,G,L,K,V,V2,W2,i.