-lemma lsubsx_inv_pair_sn_gen: ∀h,g,I,G,K1,L2,V. G ⊢ K1.ⓑ{I}V ⊆ⓧ[h, g] L2 →
- ∨∨ ∃∃f,K2. G ⊢ K1 ⊆ⓧ[h, f] K2 & g = ⫯f & L2 = K2.ⓑ{I}V
- | ∃∃f,K2. G ⊢ ⬈*[h, V] 𝐒⦃K2⦄ &
- G ⊢ K1 ⊆ⓧ[h, f] K2 & g = ↑f & L2 = K2.ⓧ.
+lemma lsubsx_inv_pair_sn_gen: ∀h,g,I,G,K1,L2,V. G ⊢ K1.ⓑ{I}V ⊆ⓧ[h,g] L2 →
+ ∨∨ ∃∃f,K2. G ⊢ K1 ⊆ⓧ[h,f] K2 & g = ⫯f & L2 = K2.ⓑ{I}V
+ | ∃∃f,K2. G ⊢ ⬈*[h,V] 𝐒⦃K2⦄ &
+ G ⊢ K1 ⊆ⓧ[h,f] K2 & g = ↑f & L2 = K2.ⓧ.