| cnv_sort: ∀G,L,s. cnv a h G L (⋆s)
| cnv_zero: ∀I,G,K,V. cnv a h G K V → cnv a h G (K.ⓑ{I}V) (#0)
| cnv_lref: ∀I,G,K,i. cnv a h G K (#i) → cnv a h G (K.ⓘ{I}) (#↑i)
| cnv_bind: ∀p,I,G,L,V,T. cnv a h G L V → cnv a h G (L.ⓑ{I}V) T → cnv a h G L (ⓑ{p,I}V.T)
| cnv_sort: ∀G,L,s. cnv a h G L (⋆s)
| cnv_zero: ∀I,G,K,V. cnv a h G K V → cnv a h G (K.ⓑ{I}V) (#0)
| cnv_lref: ∀I,G,K,i. cnv a h G K (#i) → cnv a h G (K.ⓘ{I}) (#↑i)
| cnv_bind: ∀p,I,G,L,V,T. cnv a h G L V → cnv a h G (L.ⓑ{I}V) T → cnv a h G L (ⓑ{p,I}V.T)