| 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.ⓘ{I}) (#0) (#0)
| cpce_eta : ∀n,p,G,K,W,V1,V2,W2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U →
| 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.ⓘ{I}) (#0) (#0)
| cpce_eta : ∀n,p,G,K,W,V1,V2,W2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U →
| cpce_lref: ∀I,G,K,T,U,i. cpce h G K (#i) T →
| cpce_lref: ∀I,G,K,T,U,i. cpce h G K (#i) T →
| cpce_gref: ∀G,L,l. cpce h G L (§l) (§l)
| cpce_bind: ∀p,I,G,K,V1,V2,T1,T2.
cpce h G K V1 V2 → cpce h G (K.ⓑ{I}V1) T1 T2 →
| cpce_gref: ∀G,L,l. cpce h G L (§l) (§l)
| cpce_bind: ∀p,I,G,K,V1,V2,T1,T2.
cpce h G K V1 V2 → cpce h G (K.ⓑ{I}V1) T1 T2 →
∀I. ⦃G,K.ⓘ{I}⦄ ⊢ #0 ⬌η[h] X2 →
∨∨ ∧∧ ∀n,p,W,V,U. I = BPair Abst W → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥ & #0 = X2
| ∃∃n,p,W,V1,V2,W2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U & ⦃G,K⦄ ⊢ V1 ⬌η[h] V2
∀I. ⦃G,K.ⓘ{I}⦄ ⊢ #0 ⬌η[h] X2 →
∨∨ ∧∧ ∀n,p,W,V,U. I = BPair Abst W → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥ & #0 = X2
| ∃∃n,p,W,V1,V2,W2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U & ⦃G,K⦄ ⊢ V1 ⬌η[h] V2
lemma cpce_inv_lref_sn (h) (G) (K) (X2):
∀I,i. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬌η[h] X2 →
lemma cpce_inv_lref_sn (h) (G) (K) (X2):
∀I,i. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬌η[h] X2 →