-lemma lpx_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 lpx_inv_pair_sn (G):
+ ∀I,L2,K1,V1. ❪G,K1.ⓑ[I]V1❫ ⊢ ⬈ L2 →
+ ∃∃K2,V2. ❪G,K1❫ ⊢ ⬈ K2 & ❪G,K1❫ ⊢ V1 ⬈ V2 & L2 = K2.ⓑ[I]V2.