-fact lsuba_inv_bind1_aux: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀I,K1. L1 = K1.ⓘ{I} →
- (∃∃K2. G ⊢ K1 ⫃⁝ K2 & L2 = K2.ⓘ{I}) ∨
- â\88\83â\88\83K2,W,V,A. â¦\83G,K1â¦\84 â\8a¢ â\93\9dW.V â\81\9d A & â¦\83G,K2â¦\84 ⊢ W ⁝ A &
+fact lsuba_inv_bind1_aux: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀I,K1. L1 = K1.ⓘ[I] →
+ (∃∃K2. G ⊢ K1 ⫃⁝ K2 & L2 = K2.ⓘ[I]) ∨
+ â\88\83â\88\83K2,W,V,A. â\9d¨G,K1â\9d© â\8a¢ â\93\9dW.V â\81\9d A & â\9d¨G,K2â\9d© ⊢ W ⁝ A &