| cpg_ell : ∀c,G,L,V1,V2,W2. cpg h c G L V1 V2 →
⬆*[1] V2 ≡ W2 → cpg h ((↓c)+𝟘𝟙) G (L.ⓛV1) (#0) W2
| cpg_lref : ∀c,I,G,L,V,T,U,i. cpg h c G L (#i) T →
| cpg_ell : ∀c,G,L,V1,V2,W2. cpg h c G L V1 V2 →
⬆*[1] V2 ≡ W2 → cpg h ((↓c)+𝟘𝟙) G (L.ⓛV1) (#0) W2
| cpg_lref : ∀c,I,G,L,V,T,U,i. cpg h c G L (#i) T →