-lemma lsuba_inv_pair1: â\88\80I,G,K1,L2,X. G â\8a¢ K1.â\93\91{I}X â\81\9dâ«\83 L2 →
- (â\88\83â\88\83K2. G â\8a¢ K1 â\81\9dâ«\83 K2 & L2 = K2.ⓑ{I}X) ∨
- â\88\83â\88\83K2,W,V,A. â¦\83G, K1â¦\84 â\8a¢ â\93\9dW.V â\81\9d A & â¦\83G, K2â¦\84 â\8a¢ W â\81\9d A & G â\8a¢ K1 â\81\9dâ«\83 K2 &
+lemma lsuba_inv_pair1: â\88\80I,G,K1,L2,X. G â\8a¢ K1.â\93\91{I}X â«\83â\81\9d L2 →
+ (â\88\83â\88\83K2. G â\8a¢ K1 â«\83â\81\9d K2 & L2 = K2.ⓑ{I}X) ∨
+ â\88\83â\88\83K2,W,V,A. â¦\83G, K1â¦\84 â\8a¢ â\93\9dW.V â\81\9d A & â¦\83G, K2â¦\84 â\8a¢ W â\81\9d A & G â\8a¢ K1 â«\83â\81\9d K2 &