-fact lsubr_inv_bind1_aux: ∀L1,L2. L1 ⫃ L2 → ∀I,K1. L1 = K1.ⓘ{I} →
- ∨∨ ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓘ{I}
- | ∃∃K2,V,W. K1 ⫃ K2 & L2 = K2.ⓛW &
- I = BPair Abbr (ⓝW.V)
- | ∃∃J1,J2,K2,V. K1 ⫃ K2 & L2 = K2.ⓤ{J2} &
- I = BPair J1 V.
+fact lsubr_inv_bind1_aux:
+ ∀L1,L2. L1 ⫃ L2 → ∀I,K1. L1 = K1.ⓘ[I] →
+ ∨∨ ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓘ[I]
+ | ∃∃K2,V,W. K1 ⫃ K2 & L2 = K2.ⓛW & I = BPair Abbr (ⓝW.V)
+ | ∃∃J1,J2,K2,V. K1 ⫃ K2 & L2 = K2.ⓤ[J2] & I = BPair J1 V.