-inductive cpr: lenv → relation term ≝
-| cpr_atom : ∀I,L. cpr L (⓪{I}) (⓪{I})
-| cpr_delta: ∀L,K,V,V2,W2,i.
- ⇩[0, i] L ≡ K. ⓓV → cpr K V V2 →
- ⇧[0, i + 1] V2 ≡ W2 → cpr L (#i) W2
-| cpr_bind : ∀a,I,L,V1,V2,T1,T2.
- cpr L V1 V2 → cpr (L. ⓑ{I} V1) T1 T2 →
- cpr L (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2)
-| cpr_flat : ∀I,L,V1,V2,T1,T2.
- cpr L V1 V2 → cpr L T1 T2 →
- cpr L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
-| cpr_zeta : ∀L,V,T1,T,T2. cpr (L.ⓓV) T1 T →
- ⇧[0, 1] T2 ≡ T → cpr L (+ⓓV. T1) T2
-| cpr_tau : ∀L,V,T1,T2. cpr L T1 T2 → cpr L (ⓝV. T1) T2
-| cpr_beta : ∀a,L,V1,V2,W,T1,T2.
- cpr L V1 V2 → cpr (L.ⓛW) T1 T2 →
- cpr L (ⓐV1. ⓛ{a}W. T1) (ⓓ{a}V2. T2)
-| cpr_theta: ∀a,L,V1,V,V2,W1,W2,T1,T2.
- cpr L V1 V → ⇧[0, 1] V ≡ V2 → cpr L W1 W2 → cpr (L.ⓓW1) T1 T2 →
- cpr L (ⓐV1. ⓓ{a}W1. T1) (ⓓ{a}W2. ⓐV2. T2)
+inductive cpr: relation4 genv lenv term term ≝
+| cpr_atom : ∀I,G,L. cpr G L (⓪{I}) (⓪{I})
+| cpr_delta: ∀G,L,K,V,V2,W2,i.
+ ⇩[0, i] L ≡ K. ⓓV → cpr G K V V2 →
+ ⇧[0, i + 1] V2 ≡ W2 → cpr G L (#i) W2
+| cpr_bind : ∀a,I,G,L,V1,V2,T1,T2.
+ cpr G L V1 V2 → cpr G (L.ⓑ{I}V1) T1 T2 →
+ cpr G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
+| cpr_flat : ∀I,G,L,V1,V2,T1,T2.
+ cpr G L V1 V2 → cpr G L T1 T2 →
+ cpr G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+| cpr_zeta : ∀G,L,V,T1,T,T2. cpr G (L.ⓓV) T1 T →
+ ⇧[0, 1] T2 ≡ T → cpr G L (+ⓓV.T1) T2
+| cpr_tau : ∀G,L,V,T1,T2. cpr G L T1 T2 → cpr G L (ⓝV.T1) T2
+| cpr_beta : ∀a,G,L,V1,V2,W1,W2,T1,T2.
+ cpr G L V1 V2 → cpr G L W1 W2 → cpr G (L.ⓛW1) T1 T2 →
+ cpr G L (ⓐV1.ⓛ{a}W1.T1) (ⓓ{a}ⓝW2.V2.T2)
+| cpr_theta: ∀a,G,L,V1,V,V2,W1,W2,T1,T2.
+ cpr G L V1 V → ⇧[0, 1] V ≡ V2 → cpr G L W1 W2 → cpr G (L.ⓓW1) T1 T2 →
+ cpr G L (ⓐV1.ⓓ{a}W1.T1) (ⓓ{a}W2.ⓐV2.T2)