-| cpce_ldef: ∀G,K,V. cpce h G (K.ⓓV) (#0) (#0)
-| cpce_ldec: ∀n,G,K,V,s. ⦃G,K⦄ ⊢ V ➡*[n,h] ⋆s →
- cpce h G (K.â\93\9bV) (#0) (#0)
-| cpce_eta : ∀n,p,G,K,V,W1,W2,T. ⦃G,K⦄ ⊢ V ➡*[n,h] ⓛ{p}W1.T →
- cpce h G K W1 W2 → cpce h G (K.ⓛV) (#0) (+ⓛW2.ⓐ#0.#1)
+| cpce_atom: ∀G,i. cpce h G (⋆) (#i) (#i)
+| cpce_zero: ∀G,K,I. (∀n,p,W,V,U. I = BPair Abst W → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) →
+ cpce h G (K.â\93\98{I}) (#0) (#0)
+| cpce_eta : ∀n,p,G,K,W,V1,V2,W2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U →
+ cpce h G K V1 V2 → ⬆*[1] V2 ≘ W2 → cpce h G (K.ⓛW) (#0) (+ⓛW2.ⓐ#0.#1)