-(*
-lemma lpx_pair: ∀h,g,I,G,K1,K2,V1,V2. ⦃G, K1⦄ ⊢ ⬈[h] K2 → ⦃G, K1⦄ ⊢ V1 ⬈[h] V2 →
- ⦃G, K1.ⓑ{I}V1⦄ ⊢ ⬈[h] K2.ⓑ{I}V2.
-/2 width=1 by lpx_sn_pair/ qed.
-*)
+
+lemma lpx_pair (G):
+ ∀K1,K2. ❪G,K1❫ ⊢ ⬈ K2 → ∀V1,V2. ❪G,K1❫ ⊢ V1 ⬈ V2 →
+ ∀I.❪G,K1.ⓑ[I]V1❫ ⊢ ⬈ K2.ⓑ[I]V2.
+/2 width=1 by lex_pair/ qed.
+