inductive crr (G:genv): relation2 lenv term ≝
| crr_delta : ∀L,K,V,i. ⬇[i] L ≡ K.ⓓV → crr G L (#i)
| crr_appl_sn: ∀L,V,T. crr G L V → crr G L (ⓐV.T)
inductive crr (G:genv): relation2 lenv term ≝
| crr_delta : ∀L,K,V,i. ⬇[i] L ≡ K.ⓓV → crr G L (#i)
| crr_appl_sn: ∀L,V,T. crr G L V → crr G L (ⓐV.T)