-inductive crr: lenv → predicate term ≝
-| crr_delta : ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → crr L (#i)
-| crr_appl_sn: ∀L,V,T. crr L V → crr L (ⓐV.T)
-| crr_appl_dx: ∀L,V,T. crr L T → crr L (ⓐV.T)
-| crr_ri2 : ∀I,L,V,T. ri2 I → crr L (②{I}V.T)
-| crr_ib2_sn : ∀a,I,L,V,T. ib2 a I → crr L V → crr L (ⓑ{a,I}V.T)
-| crr_ib2_dx : ∀a,I,L,V,T. ib2 a I → crr (L.ⓑ{I}V) T → crr L (ⓑ{a,I}V.T)
-| crr_beta : ∀a,L,V,W,T. crr L (ⓐV. ⓛ{a}W.T)
-| crr_theta : ∀a,L,V,W,T. crr L (ⓐV. ⓓ{a}W.T)
+inductive crr (G:genv): relation2 lenv term ≝
+| crr_delta : ∀L,K,V,i. ⇩[0, i] L ≡ K.ⓓV → crr G L (#i)
+| crr_appl_sn: ∀L,V,T. crr G L V → crr G L (ⓐV.T)
+| crr_appl_dx: ∀L,V,T. crr G L T → crr G L (ⓐV.T)
+| crr_ri2 : ∀I,L,V,T. ri2 I → crr G L (②{I}V.T)
+| crr_ib2_sn : ∀a,I,L,V,T. ib2 a I → crr G L V → crr G L (ⓑ{a,I}V.T)
+| crr_ib2_dx : ∀a,I,L,V,T. ib2 a I → crr G (L.ⓑ{I}V) T → crr G L (ⓑ{a,I}V.T)
+| crr_beta : ∀a,L,V,W,T. crr G L (ⓐV.ⓛ{a}W.T)
+| crr_theta : ∀a,L,V,W,T. crr G L (ⓐV.ⓓ{a}W.T)