+
+lemma lsx_ge_up: ∀h,g,G,L,T,U,lt,l,m. lt ≤ yinj l + yinj m →
+ ⬆[l, m] T ≡ U → G ⊢ ⬊*[h, g, U, lt] L → G ⊢ ⬊*[h, g, U, l] L.
+#h #g #G #L #T #U #lt #l #m #Hltlm #HTU #H @(lsx_ind … H) -L
+/5 width=7 by lsx_intro, lleq_ge_up/
+qed-.
+
+lemma lsx_ge: ∀h,g,G,L,T,l1,l2. l1 ≤ l2 →
+ G ⊢ ⬊*[h, g, T, l1] L → G ⊢ ⬊*[h, g, T, l2] L.
+#h #g #G #L #T #l1 #l2 #Hl12 #H @(lsx_ind … H) -L
+/5 width=7 by lsx_intro, lleq_ge/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lsx_fwd_bind_sn: ∀h,g,a,I,G,L,V,T,l. G ⊢ ⬊*[h, g, ⓑ{a,I}V.T, l] L →
+ G ⊢ ⬊*[h, g, V, l] L.
+#h #g #a #I #G #L #V #T #l #H @(lsx_ind … H) -L
+#L1 #_ #IHL1 @lsx_intro
+#L2 #HL12 #HV @IHL1 /3 width=4 by lleq_fwd_bind_sn/
+qed-.
+
+lemma lsx_fwd_flat_sn: ∀h,g,I,G,L,V,T,l. G ⊢ ⬊*[h, g, ⓕ{I}V.T, l] L →
+ G ⊢ ⬊*[h, g, V, l] L.
+#h #g #I #G #L #V #T #l #H @(lsx_ind … H) -L
+#L1 #_ #IHL1 @lsx_intro
+#L2 #HL12 #HV @IHL1 /3 width=3 by lleq_fwd_flat_sn/
+qed-.
+
+lemma lsx_fwd_flat_dx: ∀h,g,I,G,L,V,T,l. G ⊢ ⬊*[h, g, ⓕ{I}V.T, l] L →
+ G ⊢ ⬊*[h, g, T, l] L.
+#h #g #I #G #L #V #T #l #H @(lsx_ind … H) -L
+#L1 #_ #IHL1 @lsx_intro
+#L2 #HL12 #HV @IHL1 /3 width=3 by lleq_fwd_flat_dx/
+qed-.
+
+lemma lsx_fwd_pair_sn: ∀h,g,I,G,L,V,T,l. G ⊢ ⬊*[h, g, ②{I}V.T, l] L →
+ G ⊢ ⬊*[h, g, V, l] L.
+#h #g * /2 width=4 by lsx_fwd_bind_sn, lsx_fwd_flat_sn/
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma lsx_inv_flat: ∀h,g,I,G,L,V,T,l. G ⊢ ⬊*[h, g, ⓕ{I}V.T, l] L →
+ G ⊢ ⬊*[h, g, V, l] L ∧ G ⊢ ⬊*[h, g, T, l] L.
+/3 width=3 by lsx_fwd_flat_sn, lsx_fwd_flat_dx, conj/ qed-.