-fact lsubf_inv_pair1_aux: ∀f1,f2,L1,L2. ⦃L1,f1⦄ ⫃𝐅* ⦃L2,f2⦄ →
- ∀g1,I,K1,X. f1 = ↑g1 → L1 = K1.ⓑ{I}X →
- ∨∨ ∃∃g2,K2. ⦃K1,g1⦄ ⫃𝐅* ⦃K2,g2⦄ & f2 = ↑g2 & L2 = K2.ⓑ{I}X
- | ∃∃g,g0,g2,K2,W,V. ⦃K1,g0⦄ ⫃𝐅* ⦃K2,g2⦄ &
- K1 ⊢ 𝐅*⦃V⦄ ≘ g & g0 ⋓ g ≘ g1 & f2 = ↑g2 &
- I = Abbr & X = ⓝW.V & L2 = K2.ⓛW
- | ∃∃g,g0,g2,J,K2. ⦃K1,g0⦄ ⫃𝐅* ⦃K2,g2⦄ &
- K1 ⊢ 𝐅*⦃X⦄ ≘ g & g0 ⋓ g ≘ g1 & f2 = ↑g2 &
- L2 = K2.ⓤ{J}.
+fact lsubf_inv_pair1_aux:
+ ∀f1,f2,L1,L2. ⦃L1,f1⦄ ⫃𝐅+ ⦃L2,f2⦄ →
+ ∀g1,I,K1,X. f1 = ↑g1 → L1 = K1.ⓑ{I}X →
+ ∨∨ ∃∃g2,K2. ⦃K1,g1⦄ ⫃𝐅+ ⦃K2,g2⦄ & f2 = ↑g2 & L2 = K2.ⓑ{I}X
+ | ∃∃g,g0,g2,K2,W,V. ⦃K1,g0⦄ ⫃𝐅+ ⦃K2,g2⦄ &
+ K1 ⊢ 𝐅+⦃V⦄ ≘ g & g0 ⋓ g ≘ g1 & f2 = ↑g2 &
+ I = Abbr & X = ⓝW.V & L2 = K2.ⓛW
+ | ∃∃g,g0,g2,J,K2. ⦃K1,g0⦄ ⫃𝐅+ ⦃K2,g2⦄ &
+ K1 ⊢ 𝐅+⦃X⦄ ≘ g & g0 ⋓ g ≘ g1 & f2 = ↑g2 & L2 = K2.ⓤ{J}.