lemma cpce_eta_drops (h) (n) (G) (K):
∀p,W,V1,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U →
∀V2. ⦃G,K⦄ ⊢ V1 ⬌η[h] V2 →
- â\88\80i,L. â¬\87*[i] L ≘ K.ⓛW →
- â\88\80W2. â¬\86*[↑i] V2 ≘ W2 → ⦃G,L⦄ ⊢ #i ⬌η[h] +ⓛW2.ⓐ#0.#↑i.
+ â\88\80i,L. â\87©*[i] L ≘ K.ⓛW →
+ â\88\80W2. â\87§*[↑i] V2 ≘ W2 → ⦃G,L⦄ ⊢ #i ⬌η[h] +ⓛW2.ⓐ#0.#↑i.
#h #n #G #K #p #W #V1 #U #HWU #V2 #HV12 #i elim i -i
[ #L #HLK #W2 #HVW2
>(drops_fwd_isid … HLK) -L [| // ] /2 width=8 by cpce_eta/
qed.
lemma cpce_zero_drops (h) (G):
- â\88\80i,L. (â\88\80n,p,K,W,V,U. â¬\87*[i] L ≘ K.ⓛW → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) →
+ â\88\80i,L. (â\88\80n,p,K,W,V,U. â\87©*[i] L ≘ K.ⓛW → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) →
⦃G,L⦄ ⊢ #i ⬌η[h] #i.
#h #G #i elim i -i
[ * [ #_ // ] #L #I #Hi