+fact lsubs_inv_skip1_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 →
+ ∀I1,K1,V1. L1 = K1.ⓑ{I1}V1 → 0 < d →
+ ∃∃I2,K2,V2. K1 ≼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
+#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 lsubs_inv_skip1: ∀I1,K1,L2,V1,d,e. K1.ⓑ{I1}V1 ≼ [d, e] L2 → 0 < d →
+ ∃∃I2,K2,V2. K1 ≼ [d - 1, e] K2 & L2 = K2.ⓑ{I2}V2.
+/2 width=5/ qed-.
+
+fact lsubs_inv_atom2_aux: ∀L1,L2,d,e. L1 ≼ [d, e] L2 → L2 = ⋆ →
+ L1 = ⋆ ∨ (d = 0 ∧ e = 0).
+#L1 #L2 #d #e * -L1 -L2 -d -e
+[ /2 width=1/
+| /3 width=1/
+| #L1 #L2 #W #e #_ #H destruct
+| #L1 #L2 #I #W1 #W2 #e #_ #H destruct
+| #L1 #L2 #I1 #I2 #W1 #W2 #d #e #_ #H destruct
+]
+qed.
+
+lemma lsubs_inv_atom2: ∀L1,d,e. L1 ≼ [d, e] ⋆ →
+ L1 = ⋆ ∨ (d = 0 ∧ e = 0).
+/2 width=3/ qed-.
+
+fact lsubs_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.