#h #o #G #L #T1 #T #T2 #d1 #d2 #d #Hd21 #HTd1 #HT1 * #T0 #d0 #Hd0 #HTd0 #HT0 #HT02
lapply (lstas_da_conf … HT1 … HTd1) #HTd12
lapply (da_mono … HTd12 … HTd0) -HTd12 -HTd0 #H destruct
-lapply (le_minus_to_plus_r … Hd21 Hd0) -Hd21 -Hd0
+lapply (le_minus_to_plus_c … Hd21 Hd0) -Hd21 -Hd0
/3 width=7 by lstas_trans, ex4_2_intro/
qed-.
qed-.
lemma scpds_inv_abbr_abst: ∀h,o,a1,a2,G,L,V1,W2,T1,T2,d. ⦃G, L⦄ ⊢ ⓓ{a1}V1.T1 •*➡*[h, o, d] ⓛ{a2}W2.T2 →
- â\88\83â\88\83T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\80¢*â\9e¡*[h, o, d] T & â¬\86[0, 1] â\93\9b{a2}W2.T2 â\89¡ T & a1 = true.
+ â\88\83â\88\83T. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\80¢*â\9e¡*[h, o, d] T & â¬\86[0, 1] â\93\9b{a2}W2.T2 â\89\98 T & a1 = true.
#h #o #a1 #a2 #G #L #V1 #W2 #T1 #T2 #d2 * #X #d1 #Hd21 #Hd1 #H1 #H2
lapply (da_inv_bind … Hd1) -Hd1 #Hd1
elim (lstas_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct