+lemma lstas_cpxs: ∀h,g,G,L,T1,T2,l2. ⦃G, L⦄ ⊢ T1 •*[h, l2] T2 →
+ ∀l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l1 → l2 ≤ l1 → ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2.
+#h #g #G #L #T1 #T2 #l2 #H elim H -G -L -T1 -T2 -l2 //
+[ /3 width=3 by cpxs_sort, da_inv_sort/
+| #G #L #K #V1 #V2 #W2 #i #l2 #HLK #_ #HVW2 #IHV12 #l1 #H #Hl21
+ elim (da_inv_lref … H) -H * #K0 #V0 [| #l0 ] #HLK0
+ lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct /3 width=7 by cpxs_delta/
+| #G #L #K #V1 #V2 #W2 #i #l2 #HLK #_ #HVW2 #IHV12 #l1 #H #Hl21
+ elim (da_inv_lref … H) -H * #K0 #V0 [| #l0 ] #HLK0
+ lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct
+ #HV1 #H destruct lapply (le_plus_to_le_r … Hl21) -Hl21
+ /3 width=7 by cpxs_delta/
+| /4 width=3 by cpxs_bind_dx, da_inv_bind/
+| /4 width=3 by cpxs_flat_dx, da_inv_flat/
+| /4 width=3 by cpxs_eps, da_inv_flat/
+]
+qed.
+