-inductive crx (h) (g) (G:genv): relation2 lenv term ≝
-| crx_sort : ∀L,k,d. deg h g k (d+1) → crx h g G L (⋆k)
-| crx_delta : ∀I,L,K,V,i. ⬇[i] L ≡ K.ⓑ{I}V → crx h g G L (#i)
-| crx_appl_sn: ∀L,V,T. crx h g G L V → crx h g G L (ⓐV.T)
-| crx_appl_dx: ∀L,V,T. crx h g G L T → crx h g G L (ⓐV.T)
-| crx_ri2 : ∀I,L,V,T. ri2 I → crx h g G L (②{I}V.T)
-| crx_ib2_sn : ∀a,I,L,V,T. ib2 a I → crx h g G L V → crx h g G L (ⓑ{a,I}V.T)
-| crx_ib2_dx : ∀a,I,L,V,T. ib2 a I → crx h g G (L.ⓑ{I}V) T → crx h g G L (ⓑ{a,I}V.T)
-| crx_beta : ∀a,L,V,W,T. crx h g G L (ⓐV. ⓛ{a}W.T)
-| crx_theta : ∀a,L,V,W,T. crx h g G L (ⓐV. ⓓ{a}W.T)
+inductive crx (h) (o) (G:genv): relation2 lenv term ≝
+| crx_sort : ∀L,s,d. deg h o s (d+1) → crx h o G L (⋆s)
+| crx_delta : ∀I,L,K,V,i. ⬇[i] L ≡ K.ⓑ{I}V → crx h o G L (#i)
+| crx_appl_sn: ∀L,V,T. crx h o G L V → crx h o G L (ⓐV.T)
+| crx_appl_dx: ∀L,V,T. crx h o G L T → crx h o G L (ⓐV.T)
+| crx_ri2 : ∀I,L,V,T. ri2 I → crx h o G L (②{I}V.T)
+| crx_ib2_sn : ∀a,I,L,V,T. ib2 a I → crx h o G L V → crx h o G L (ⓑ{a,I}V.T)
+| crx_ib2_dx : ∀a,I,L,V,T. ib2 a I → crx h o G (L.ⓑ{I}V) T → crx h o G L (ⓑ{a,I}V.T)
+| crx_beta : ∀a,L,V,W,T. crx h o G L (ⓐV. ⓛ{a}W.T)
+| crx_theta : ∀a,L,V,W,T. crx h o G L (ⓐV. ⓓ{a}W.T)