-lemma cpg_inv_bind1: ∀Rt,c,h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[Rt, c, h] U2 →
- ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 &
+lemma cpg_inv_bind1: ∀Rt,c,h,p,I,G,L,V1,T1,U2. ⦃G,L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[Rt,c,h] U2 →
+ ∨∨ ∃∃cV,cT,V2,T2. ⦃G,L⦄ ⊢ V1 ⬈[Rt,cV,h] V2 & ⦃G,L.ⓑ{I}V1⦄ ⊢ T1 ⬈[Rt,cT,h] T2 &