-qed.
-
-lemma lsubr_inv_atom2: ∀L1,d,e. L1 ≼ [d, e] ⋆ →
- L1 = ⋆ ∨ (d = 0 ∧ e = 0).
-/2 width=3/ qed-.
-
-fact lsubr_inv_abbr2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
- ∀K2,V. L2 = K2.ⓓV → d = 0 → 0 < e →
- ∃∃K1. K1 ≼ [0, e - 1] K2 & L1 = K1.ⓓV.
-#L1 #L2 #d #e * -L1 -L2 -d -e
-[ #d #e #K1 #V #H destruct
-| #L1 #L2 #K1 #V #_ #_ #H
- elim (lt_zero_false … H)
-| #L1 #L2 #W #e #HL12 #K1 #V #H #_ #_ destruct /2 width=3/
-| #L1 #L2 #I #W1 #W2 #e #_ #K1 #V #H destruct
-| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #K1 #V #_ >commutative_plus normalize #H destruct
-]
-qed.
-
-lemma lsubr_inv_abbr2: ∀L1,K2,V,e. L1 ≼ [0, e] K2.ⓓV → 0 < e →
- ∃∃K1. K1 ≼ [0, e - 1] K2 & L1 = K1.ⓓV.
-/2 width=5/ qed-.
-
-fact lsubr_inv_skip2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
- ∀I2,K2,V2. L2 = K2.ⓑ{I2}V2 → 0 < d →
- ∃∃I1,K1,V1. K1 ≼ [d - 1, e] K2 & L1 = K1.ⓑ{I1}V1.
-#L1 #L2 #d #e * -L1 -L2 -d -e
-[ #d #e #I1 #K1 #V1 #H destruct
-| #L1 #L2 #I1 #K1 #V1 #_ #H
- elim (lt_zero_false … H)
-| #L1 #L2 #W #e #_ #I1 #K1 #V1 #_ #H
- elim (lt_zero_false … H)
-| #L1 #L2 #I #W1 #W2 #e #_ #I1 #K1 #V1 #_ #H
- elim (lt_zero_false … H)
-| #L1 #L2 #J1 #J2 #W1 #W2 #d #e #HL12 #I1 #K1 #V1 #H #_ destruct /2 width=5/
+qed-.
+
+lemma lsubr_inv_abbr2: ∀L1,K2,W. L1 ⊑ K2.ⓓW →
+ ∃∃K1. K1 ⊑ K2 & L1 = K1.ⓓW.
+/2 width=3 by lsubr_inv_abbr2_aux/ qed-.
+
+fact lsubr_inv_abst2_aux: ∀L1,L2. L1 ⊑ L2 → ∀K2,W2. L2 = K2.ⓛW2 →
+ ∃∃I,K1,W1. K1 ⊑ K2 & L1 = K1.ⓑ{I}W1.
+#L1 #L2 * -L1 -L2
+[ #L #K2 #W2 #H destruct
+| #L1 #L2 #V #_ #K2 #W2 #H destruct
+| #I #L1 #L2 #V1 #V2 #HL12 #K2 #W2 #H destruct /2 width=5/