-lemma cpg_ell_drops: â\88\80Rt,c,h,G,K,V,V2,i,L,T2. â\87©*[i] L â\89\98 K.â\93\9bV â\86\92 â¦\83G,Kâ¦\84 ⊢ V ⬈[Rt,c,h] V2 →
- â\87§*[â\86\91i] V2 â\89\98 T2 â\86\92 â¦\83G,Lâ¦\84 ⊢ #i ⬈[Rt,c+𝟘𝟙,h] T2.
+lemma cpg_ell_drops: â\88\80Rt,c,h,G,K,V,V2,i,L,T2. â\87©*[i] L â\89\98 K.â\93\9bV â\86\92 â\9dªG,Kâ\9d« ⊢ V ⬈[Rt,c,h] V2 →
+ â\87§*[â\86\91i] V2 â\89\98 T2 â\86\92 â\9dªG,Lâ\9d« ⊢ #i ⬈[Rt,c+𝟘𝟙,h] T2.