-inductive cpx (h) (g): lenv → relation term ≝
-| cpx_atom : ∀I,L. cpx h g L (⓪{I}) (⓪{I})
-| cpx_sort : ∀L,k,l. deg h g k (l+1) → cpx h g L (⋆k) (⋆(next h k))
-| cpx_delta: ∀I,L,K,V,V2,W2,i.
- ⇩[0, i] L ≡ K.ⓑ{I}V → cpx h g K V V2 →
- ⇧[0, i + 1] V2 ≡ W2 → cpx h g L (#i) W2
-| cpx_bind : ∀a,I,L,V1,V2,T1,T2.
- cpx h g L V1 V2 → cpx h g (L. ⓑ{I} V1) T1 T2 →
- cpx h g L (ⓑ{a,I} V1. T1) (ⓑ{a,I} V2. T2)
-| cpx_flat : ∀I,L,V1,V2,T1,T2.
- cpx h g L V1 V2 → cpx h g L T1 T2 →
- cpx h g L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
-| cpx_zeta : ∀L,V,T1,T,T2. cpx h g (L.ⓓV) T1 T →
- ⇧[0, 1] T2 ≡ T → cpx h g L (+ⓓV. T1) T2
-| cpx_tau : ∀L,V,T1,T2. cpx h g L T1 T2 → cpx h g L (ⓝV. T1) T2
-| cpx_beta : ∀a,L,V1,V2,W,T1,T2.
- cpx h g L V1 V2 → cpx h g (L.ⓛW) T1 T2 →
- cpx h g L (ⓐV1. ⓛ{a}W. T1) (ⓓ{a}V2. T2)
-| cpx_theta: ∀a,L,V1,V,V2,W1,W2,T1,T2.
- cpx h g L V1 V → ⇧[0, 1] V ≡ V2 → cpx h g L W1 W2 → cpx h g (L.ⓓW1) T1 T2 →
- cpx h g L (ⓐV1. ⓓ{a}W1. T1) (ⓓ{a}W2. ⓐV2. T2)
+(* avtivate genv *)
+inductive cpx (h) (g): relation4 genv lenv term term ≝
+| cpx_atom : ∀I,G,L. cpx h g G L (⓪{I}) (⓪{I})
+| cpx_sort : ∀G,L,k,l. deg h g k (l+1) → cpx h g G L (⋆k) (⋆(next h k))
+| cpx_delta: ∀I,G,L,K,V,V2,W2,i.
+ ⇩[0, i] L ≡ K.ⓑ{I}V → cpx h g G K V V2 →
+ ⇧[0, i + 1] V2 ≡ W2 → cpx h g G L (#i) W2
+| cpx_bind : ∀a,I,G,L,V1,V2,T1,T2.
+ cpx h g G L V1 V2 → cpx h g G (L.ⓑ{I}V1) T1 T2 →
+ cpx h g G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
+| cpx_flat : ∀I,G,L,V1,V2,T1,T2.
+ cpx h g G L V1 V2 → cpx h g G L T1 T2 →
+ cpx h g G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
+| cpx_zeta : ∀G,L,V,T1,T,T2. cpx h g G (L.ⓓV) T1 T →
+ ⇧[0, 1] T2 ≡ T → cpx h g G L (+ⓓV.T1) T2
+| cpx_tau : ∀G,L,V,T1,T2. cpx h g G L T1 T2 → cpx h g G L (ⓝV.T1) T2
+| cpx_ti : ∀G,L,V1,V2,T. cpx h g G L V1 V2 → cpx h g G L (ⓝV1.T) V2
+| cpx_beta : ∀a,G,L,V1,V2,W1,W2,T1,T2.
+ cpx h g G L V1 V2 → cpx h g G L W1 W2 → cpx h g G (L.ⓛW1) T1 T2 →
+ cpx h g G L (ⓐV1.ⓛ{a}W1.T1) (ⓓ{a}ⓝW2.V2.T2)
+| cpx_theta: ∀a,G,L,V1,V,V2,W1,W2,T1,T2.
+ cpx h g G L V1 V → ⇧[0, 1] V ≡ V2 → cpx h g G L W1 W2 →
+ cpx h g G (L.ⓓW1) T1 T2 →
+ cpx h g G L (ⓐV1.ⓓ{a}W1.T1) (ⓓ{a}W2.ⓐV2.T2)