+(* Advanced properties ******************************************************)
+
+lemma ssta_cpx: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •[h, g] T2 →
+ ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
+#h #g #G #L #T1 #T2 #l #H elim H -G -L -T1 -T2
+[ #G #L #k #H lapply (da_inv_sort … H) -H /2 width=2/
+| #G #L #K #V #U #W #i #HLK #_ #HWU #IHVW #H
+ elim (da_inv_lref … H) -H * #K0 #V0 [| #l0 ] #HLK0
+ lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct /3 width=7/
+| #G #L #K #W #U #l0 #i #HLK #_ #HWU #H
+ elim (da_inv_lref … H) -H * #K0 #W0 [| #l1 ] #HLK0
+ lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct /2 width=7/
+| #a #I #G #L #V #T #U #_ #IHTU #H lapply (da_inv_bind … H) -H /3 width=1/
+| #G #L #V #T #U #_ #IHTU #H lapply (da_inv_flat … H) -H /3 width=1/
+| #G #L #W #T #U #_ #IHTU #H lapply (da_inv_flat … H) -H /3 width=1/
+]
+qed.
+