-theorem lstas_conf_le: ∀h,G,L,T,U1,l1. ⦃G, L⦄ ⊢ T •*[h, l1] U1 →
- ∀U2,l2. l1 ≤ l2 → ⦃G, L⦄ ⊢ T •*[h, l2] U2 →
- ⦃G, L⦄ ⊢ U1 •*[h, l2-l1] U2.
-#h #G #L #T #U1 #l1 #HTU1 #U2 #l2 #Hl12
->(plus_minus_m_m … Hl12) in ⊢ (%→?); -Hl12 >commutative_plus #H
-elim (lstas_split … H) -H #U #HTU
->(lstas_mono … HTU … HTU1) -T //
+(* Advanced inversion lemmas ************************************************)
+
+(* Basic_1: was just: sty0_correct *)
+lemma lstas_correct: ∀h,G,L,T1,T,d1. ⦃G, L⦄ ⊢ T1 •*[h, d1] T →
+ ∀d2. ∃T2. ⦃G, L⦄ ⊢ T •*[h, d2] T2.
+#h #G #L #T1 #T #d1 #H elim H -G -L -T1 -T -d1
+[ /2 width=2 by lstas_sort, ex_intro/
+| #G #L #K #V1 #V #U #i #d #HLK #_ #HVU #IHV1 #d2
+ elim (IHV1 d2) -IHV1 #V2
+ elim (lift_total V2 0 (i+1))
+ lapply (drop_fwd_drop2 … HLK) -HLK
+ /3 width=11 by ex_intro, lstas_lift/
+| #G #L #K #W1 #W #i #HLK #HW1 #IHW1 #d2
+ @(nat_ind_plus … d2) -d2 /3 width=5 by lstas_zero, ex_intro/
+ #d2 #_ elim (IHW1 d2) -IHW1 #W2 #HW2
+ lapply (lstas_trans … HW1 … HW2) -W
+ elim (lift_total W2 0 (i+1))
+ /3 width=7 by lstas_succ, ex_intro/
+| #G #L #K #W1 #W #U #i #d #HLK #_ #HWU #IHW1 #d2
+ elim (IHW1 d2) -IHW1 #W2
+ elim (lift_total W2 0 (i+1))
+ lapply (drop_fwd_drop2 … HLK) -HLK
+ /3 width=11 by ex_intro, lstas_lift/
+| #a #I #G #L #V #T #U #d #_ #IHTU #d2
+ elim (IHTU d2) -IHTU /3 width=2 by lstas_bind, ex_intro/
+| #G #L #V #T #U #d #_ #IHTU #d2
+ elim (IHTU d2) -IHTU /3 width=2 by lstas_appl, ex_intro/
+| #G #L #W #T #U #d #_ #IHTU #d2
+ elim (IHTU d2) -IHTU /2 width=2 by ex_intro/
+]