-lemma lsubc_inv_pair2: ∀RP,I,G,L1,K2,W. G ⊢ L1 ⫃[RP] K2.ⓑ{I} W →
- (â\88\83â\88\83K1. G â\8a¢ K1 â«\83[RP] K2 & L1 = K1.â\93\91{I} W) ∨
- ∃∃K1,V,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A &
- G ⊢ K1 ⫃[RP] K2 &
- L1 = K1.ⓓⓝW.V & I = Abst.
-/2 width=3 by lsubc_inv_pair2_aux/ qed-.
+lemma lsubc_inv_bind2: ∀RP,I,G,L1,K2. G ⊢ L1 ⫃[RP] K2.ⓘ{I} →
+ (â\88\83â\88\83K1. G â\8a¢ K1 â«\83[RP] K2 & L1 = K1.â\93\98{I}) ∨
+ ∃∃K1,V,W,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A &
+ G ⊢ K1 ⫃[RP] K2 &
+ L1 = K1.ⓓⓝW.V & I = BPair Abst W.
+/2 width=3 by lsubc_inv_bind2_aux/ qed-.