-qed.
-
-(* Basic_1: was: csubc_gen_sort_r *)
-lemma lsubc_inv_atom1: ∀RP,L2. ⋆ ⊑[RP] L2 → L2 = ⋆.
-/2 width=4/ qed-.
-
-fact lsubc_inv_pair1_aux: ∀RP,L1,L2. L1 ⊑[RP] L2 → ∀I,K1,V. L1 = K1. ⓑ{I} V →
- (∃∃K2. K1 ⊑[RP] K2 & L2 = K2. ⓑ{I} V) ∨
- ∃∃K2,W,A. ⦃K1, V⦄ ϵ[RP] 〚A〛 & K2 ⊢ W ⁝ A &
- K1 ⊑[RP] K2 &
- L2 = K2. ⓛW & I = Abbr.
-#RP #L1 #L2 * -L1 -L2
+qed-.
+
+(* Basic_1: was just: csubc_gen_sort_r *)
+lemma lsubc_inv_atom1: ∀RP,G,L2. G ⊢ ⋆ ⫃[RP] L2 → L2 = ⋆.
+/2 width=5 by lsubc_inv_atom1_aux/ qed-.
+
+fact lsubc_inv_pair1_aux: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
+ (∃∃K2. G ⊢ K1 ⫃[RP] K2 & L2 = K2.ⓑ{I}X) ∨
+ ∃∃K2,V,W,A. ⦃G, K1, V⦄ ϵ[RP] 〚A〛 & ⦃G, K1, W⦄ ϵ[RP] 〚A〛 & ⦃G, K2⦄ ⊢ W ⁝ A &
+ G ⊢ K1 ⫃[RP] K2 &
+ L2 = K2. ⓛW & X = ⓝW.V & I = Abbr.
+#RP #G #L1 #L2 * -L1 -L2