matita/matita/contribs/lambdadelta/basic_2/etc/da/da_lift.etc

   1 (* Advanced properties ******************************************************)
   2
   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
   6 [ #G #L #k #l #H
   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/
  22 ]
  23 qed-.