-lemma lsuba_inv_pair2: ∀I,G,L1,K2,W. G ⊢ L1 ⫃⁝ K2.ⓑ{I}W →
- (â\88\83â\88\83K1. G â\8a¢ K1 â«\83â\81\9d K2 & L1 = K1.â\93\91{I}W) ∨
- ∃∃K1,V,A. ⦃G, K1⦄ ⊢ ⓝW.V ⁝ A & ⦃G, K2⦄ ⊢ W ⁝ A & G ⊢ K1 ⫃⁝ K2 &
- I = Abst & L1 = K1.ⓓⓝW.V.
-/2 width=3 by lsuba_inv_pair2_aux/ qed-.
+lemma lsuba_inv_bind2: ∀I,G,L1,K2. G ⊢ L1 ⫃⁝ K2.ⓘ{I} →
+ (â\88\83â\88\83K1. G â\8a¢ K1 â«\83â\81\9d K2 & L1 = K1.â\93\98{I}) ∨
+ ∃∃K1,V,W,A. ⦃G, K1⦄ ⊢ ⓝW.V ⁝ A & ⦃G, K2⦄ ⊢ W ⁝ A & G ⊢ K1 ⫃⁝ K2 &
+ I = BPair Abst W & L1 = K1.ⓓⓝW.V.
+/2 width=3 by lsuba_inv_bind2_aux/ qed-.