-lemma lpxs_inv_pair_sn (h) (G): ∀I,L2,K1,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢⬈*[h] L2 →
- ∃∃K2,V2. ⦃G, K1⦄ ⊢⬈*[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈*[h] V2 & L2 = K2.ⓑ{I}V2.
+lemma lpxs_inv_pair_sn (h) (G): ∀I,L2,K1,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ⬈*[h] L2 →
+ ∃∃K2,V2. ⦃G, K1⦄ ⊢ ⬈*[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈*[h] V2 & L2 = K2.ⓑ{I}V2.