lemma lsubf_inv_pair1: ∀g1,f2,I,K1,L2,X. ⦃K1.ⓑ{I}X, ⫯g1⦄ ⫃𝐅* ⦃L2, f2⦄ →
∨∨ ∃∃g2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ⫯g2 & L2 = K2.ⓑ{I}X
| ∃∃g,g0,g2,K2,W,V. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ &
lemma lsubf_inv_pair1: ∀g1,f2,I,K1,L2,X. ⦃K1.ⓑ{I}X, ⫯g1⦄ ⫃𝐅* ⦃L2, f2⦄ →
∨∨ ∃∃g2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ⫯g2 & L2 = K2.ⓑ{I}X
| ∃∃g,g0,g2,K2,W,V. ⦃K1, g0⦄ ⫃𝐅* ⦃K2, g2⦄ &