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