-lemma lsuba_inv_atom1: ∀L2. ⋆ ⁝⊑ L2 → L2 = ⋆.
-/2 width=3 by lsuba_inv_atom1_aux/ qed-.
-
-fact lsuba_inv_pair1_aux: ∀L1,L2. L1 ⁝⊑ L2 → ∀I,K1,X. L1 = K1.ⓑ{I}X →
- (∃∃K2. K1 ⁝⊑ K2 & L2 = K2.ⓑ{I}X) ∨
- ∃∃K2,W,V,A. K1 ⊢ ⓝW.V ⁝ A & K2 ⊢ W ⁝ A & K1 ⁝⊑ K2 &
- I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
-#L1 #L2 * -L1 -L2
-[ #J #K1 #X #H destruct
-| #I #L1 #L2 #V #HL12 #J #K1 #X #H destruct /3 width=3/
-| #L1 #L2 #W #V #A #HV #HW #HL12 #J #K1 #X #H destruct /3 width=9/
+lemma lsuba_inv_atom1: ∀G,L2. G ⊢ ⋆ ⫃⁝ L2 → L2 = ⋆.
+/2 width=4 by lsuba_inv_atom1_aux/ qed-.
+
+fact lsuba_inv_bind1_aux: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → ∀I,K1. L1 = K1.ⓘ{I} →
+ (∃∃K2. G ⊢ K1 ⫃⁝ K2 & L2 = K2.ⓘ{I}) ∨
+ ∃∃K2,W,V,A. ⦃G, K1⦄ ⊢ ⓝW.V ⁝ A & ⦃G, K2⦄ ⊢ W ⁝ A &
+ G ⊢ K1 ⫃⁝ K2 & I = BPair Abbr (ⓝW.V) & L2 = K2.ⓛW.
+#G #L1 #L2 * -L1 -L2
+[ #J #K1 #H destruct
+| #I #L1 #L2 #HL12 #J #K1 #H destruct /3 width=3 by ex2_intro, or_introl/
+| #L1 #L2 #W #V #A #HV #HW #HL12 #J #K1 #H destruct /3 width=9 by ex5_4_intro, or_intror/