-inductive crx (h) (g): lenv → predicate term ≝
-| crx_sort : ∀L,k,l. deg h g k (l+1) → crx h g L (⋆k)
-| crx_delta : ∀I,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → crx h g L (#i)
-| crx_appl_sn: ∀L,V,T. crx h g L V → crx h g L (ⓐV.T)
-| crx_appl_dx: ∀L,V,T. crx h g L T → crx h g L (ⓐV.T)
-| crx_ri2 : ∀I,L,V,T. ri2 I → crx h g L (②{I}V.T)
-| crx_ib2_sn : ∀a,I,L,V,T. ib2 a I → crx h g L V → crx h g L (ⓑ{a,I}V.T)
-| crx_ib2_dx : ∀a,I,L,V,T. ib2 a I → crx h g (L.ⓑ{I}V) T → crx h g L (ⓑ{a,I}V.T)
-| crx_beta : ∀a,L,V,W,T. crx h g L (ⓐV. ⓛ{a}W.T)
-| crx_theta : ∀a,L,V,W,T. crx h g L (ⓐV. ⓓ{a}W.T)
+inductive crx (h) (g) (G:genv): relation2 lenv term ≝
+| crx_sort : ∀L,k,l. deg h g k (l+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)