-lemma cir_inv_ib2: ∀a,I,G,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ 𝐈⦃ⓑ{a,I}V.T⦄ →
- ⦃G, L⦄ ⊢ 𝐈⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ 𝐈⦃T⦄.
-/4 width=1/ qed-.
+lemma cir_inv_ib2: ∀a,I,G,L,V,T. ib2 a I → ⦃G, L⦄ ⊢ ➡ 𝐈⦃ⓑ{a,I}V.T⦄ →
+ ⦃G, L⦄ ⊢ ➡ 𝐈⦃V⦄ ∧ ⦃G, L.ⓑ{I}V⦄ ⊢ ➡ 𝐈⦃T⦄.
+/4 width=1 by crr_ib2_sn, crr_ib2_dx, conj/ qed-.