-lemma lsubc_inv_pair1: ∀RP,I,K1,L2,V. K1. ⓑ{I} V ⊑[RP] L2 →
- (∃∃K2. K1 ⊑[RP] K2 & L2 = K2. ⓑ{I} V) ∨
- ∃∃K2,W,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
- K1 ⊑[RP] K2 &
- L2 = K2. ⓛW & I = Abbr.
-/2 width=3/ qed-.
+lemma lsubc_inv_pair1: ∀RP,I,K1,L2,X. K1.ⓑ{I}X ⊑[RP] L2 →
+ (∃∃K2. K1 ⊑[RP] K2 & L2 = K2.ⓑ{I}X) ∨
+ ∃∃K2,V,W,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & ⦃K1, W⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
+ K1 ⊑[RP] K2 &
+ L2 = K2. ⓛW & X = ⓝW.V & I = Abbr.
+/2 width=3 by lsubc_inv_pair1_aux/ qed-.