-lemma lsubv_inv_bind_sn (a) (h) (G): ∀I,K1,L2. G ⊢ K1.ⓘ{I} ⫃![a,h] L2 →
- ∨∨ ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & L2 = K2.ⓘ{I}
- | ∃∃K2,W,V. ⦃G,K1⦄ ⊢ ⓝW.V ![a,h] &
- G ⊢ K1 ⫃![a,h] K2 &
- I = BPair Abbr (ⓝW.V) & L2 = K2.ⓛW.
+lemma lsubv_inv_bind_sn (a) (h) (G):
+ ∀I,K1,L2. G ⊢ K1.ⓘ{I} ⫃![a,h] L2 →
+ ∨∨ ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & L2 = K2.ⓘ{I}
+ | ∃∃K2,W,V. ⦃G,K1⦄ ⊢ ⓝW.V ![a,h] & G ⊢ K1 ⫃![a,h] K2
+ & I = BPair Abbr (ⓝW.V) & L2 = K2.ⓛW.