-lemma cir_ib2: ∀a,I,L,V,T. ib2 a I → L ⊢ 𝐈⦃V⦄ → L.ⓑ{I}V ⊢ 𝐈⦃T⦄ → L ⊢ 𝐈⦃ⓑ{a,I}V.T⦄.
-#a #I #L #V #T #HI #HV #HT #H
-elim (crr_inv_ib2 … HI H) -HI -H /2 width=1/
+lemma cir_ib2: ∀a,I,G,L,V,T.
+ ib2 a I → ⦃G, L⦄ ⊢ ➡ 𝐈⦃V⦄ → ⦃G, L.ⓑ{I}V⦄ ⊢ ➡ 𝐈⦃T⦄ → ⦃G, L⦄ ⊢ ➡ 𝐈⦃ⓑ{a,I}V.T⦄.
+#a #I #G #L #V #T #HI #HV #HT #H
+elim (crr_inv_ib2 … HI H) -HI -H /2 width=1 by/