1 (* Advanced properties ******************************************************)
3 lemma sta_da_conf: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h] U →
4 ∀l. ⦃G, L⦄ ⊢ T ▪[h, g] l → ⦃G, L⦄ ⊢ U ▪[h, g] l-1.
5 #h #g #G #L #T #U #H elim H -G -L -T -U
7 lapply (da_inv_sort … H) -H /3 width=1/
8 | #G #L #K #V #W #W0 #i #HLK #_ #HW0 #IHVW #l #H
9 elim (da_inv_lref … H) -H * #K0 #V0 [2: #l0] #HLK0 #HV0 [ #H0 ]
10 lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct
11 lapply (ldrop_fwd_ldrop2 … HLK) -HLK /3 width=7/
12 | #G #L #K #W #V #W0 #i #HLK #HWV #HW0 #_ #l #H
13 elim (da_inv_lref … H) -H * #K0 #V0 [2: #l0] #HLK0 #HV0 [ #H0 ]
14 lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct
15 lapply (ldrop_fwd_ldrop2 … HLK) -HLK /3 width=7/
16 | #a #I #G #L #V #T #U #_ #IHTU #l #H
17 lapply (da_inv_bind … H) -H /3 width=1/
18 | #G #L #V #T #U #_ #IHTU #l #H
19 lapply (da_inv_flat … H) -H /3 width=1/
20 | #G #L #W #T #U #_ #IHTU #l #H
21 lapply (da_inv_flat … H) -H /2 width=1/