-lemma lpx_inv_pair: ∀h,I1,I2,G,L1,L2,V1,V2. ⦃G, L1.ⓑ{I1}V1⦄ ⊢ ⬈[h] L2.ⓑ{I2}V2 →
- ∧∧ ⦃G, L1⦄ ⊢ ⬈[h] L2 & ⦃G, L1⦄ ⊢ V1 ⬈[h] V2 & I1 = I2.
+lemma lpx_inv_unit_sn (G):
+ ∀I,L2,K1. ❪G,K1.ⓤ[I]❫ ⊢ ⬈ L2 →
+ ∃∃K2. ❪G,K1❫ ⊢ ⬈ K2 & L2 = K2.ⓤ[I].
+/2 width=1 by lex_inv_unit_sn/ qed-.
+
+(* Basic_2A1: was: lpx_inv_pair1 *)
+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.
+/2 width=1 by lex_inv_pair_sn/ qed-.
+
+lemma lpx_inv_unit_dx (G):
+ ∀I,L1,K2. ❪G,L1❫ ⊢ ⬈ K2.ⓤ[I] →
+ ∃∃K1. ❪G,K1❫ ⊢ ⬈ K2 & L1 = K1.ⓤ[I].
+/2 width=1 by lex_inv_unit_dx/ qed-.
+
+(* Basic_2A1: was: lpx_inv_pair2 *)
+lemma lpx_inv_pair_dx (G):
+ ∀I,L1,K2,V2. ❪G,L1❫ ⊢ ⬈ K2.ⓑ[I]V2 →
+ ∃∃K1,V1. ❪G,K1❫ ⊢ ⬈ K2 & ❪G,K1❫ ⊢ V1 ⬈ V2 & L1 = K1.ⓑ[I]V1.
+/2 width=1 by lex_inv_pair_dx/ qed-.
+
+lemma lpx_inv_pair (G):
+ ∀I1,I2,L1,L2,V1,V2. ❪G,L1.ⓑ[I1]V1❫ ⊢ ⬈ L2.ⓑ[I2]V2 →
+ ∧∧ ❪G,L1❫ ⊢ ⬈ L2 & ❪G,L1❫ ⊢ V1 ⬈ V2 & I1 = I2.