-lemma cix_inv_bind: ∀h,g,a,I,L,V,T. ⦃h, L⦄ ⊢ 𝐈[g]⦃ⓑ{a,I}V.T⦄ →
- ∧∧ ⦃h, L⦄ ⊢ 𝐈[g]⦃V⦄ & ⦃h, L.ⓑ{I}V⦄ ⊢ 𝐈[g]⦃T⦄ & ib2 a I.
+lemma cix_inv_bind: ∀h,g,a,I,L,V,T. ⦃G, L⦄ ⊢ 𝐈[h, g]⦃ⓑ{a,I}V.T⦄ →
+ ∧∧ ⦃G, L⦄ ⊢ 𝐈[h, g]⦃V⦄ & ⦃h, L.ⓑ{I}V⦄ ⊢ 𝐈[h, g]⦃T⦄ & ib2 a I.