-fact lsubv_inv_bind_dx_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 →
- ∀I,K2. L2 = 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.
-#a #h #G #L1 #L2 * -L1 -L2
+fact lsubv_inv_bind_dx_aux (h) (a) (G):
+ ∀L1,L2. G ⊢ L1 ⫃![h,a] L2 →
+ ∀I,K2. L2 = 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.
+#h #a #G #L1 #L2 * -L1 -L2