#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
#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