matita/matita/contribs/lambdadelta/basic_2/etc/frees/frees_drops2.etc

   1 include "basic_2/static/frees_drops.ma".
   2
   3 axiom frees_inv_drops_next_sle: ∀f1,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → ∀f2. f1 ⊆ f2 →
   4                                 ∀I2,L2,V2,n. ⬇*[n] L1 ≡ L2.ⓑ{I2}V2 →
   5                                 ∀g1. ⫯g1 = ⫱*[n] f1 →
   6                                 ∀g2. L2 ⊢ 𝐅*⦃V2⦄ ≡ g2 → ↑*[n]⫯g2 ⊆ f2.
   7
   8 lemma frees_drops_next_sle: ∀f1,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → ∀f2. (
   9                                ∀n. ⬇*[Ⓕ, 𝐔❴n❵] L1 ≡ ⋆ →
  10                                ∀g1. ⫯g1 = ⫱*[n] f1 →
  11                                ∀g2. 𝐈⦃g2⦄ → ↑*[n]⫯g2 ⊆ f2
  12                             ) → (
  13                                ∀I2,L2,V2,n. ⬇*[n] L1 ≡ L2.ⓑ{I2}V2 →
  14                                ∀g1. ⫯g1 = ⫱*[n] f1 →
  15                                ∀g2. L2 ⊢ 𝐅*⦃V2⦄ ≡ g2 → ↑*[n]⫯g2 ⊆ f2
  16                             ) → (
  17                                ∀I2,L2,n. ⬇*[n] L1 ≡ L2.ⓤ{I2} →
  18                                ∀g1. ⫯g1 = ⫱*[n] f1 →
  19                                ∀g2. 𝐈⦃g2⦄ → ↑*[n]⫯g2 ⊆ f2
  20                             ) → f1 ⊆ f2.
  21 #f1 #L1 #T1 #H @(frees_ind_void … H) -f1 -L1 -T1
  22 [ /2 width=1 by sle_isid_sn/
  23 | /2 width=2 by/
  24 | /3 width=5 by drops_refl/
  25 | /3 width=3 by drops_refl/
  26 | /6 width=5 by drops_drop, sle_inv_tl_dx, sle_px_tl/
  27 | /2 width=1 by sle_isid_sn/
  28 | #f1a #f1b #f1 #p #I1 #L1 #V1 #T1 #_ #_ #Hf1 #IHa #IHb #f2 #H1 #H2 #H3
  29   lapply (sor_tls … Hf1) #Hn
  30   @(sor_inv_sle … Hf1) -Hf1
  31   [ @IHa -IHa -IHb [| #I2 #L2 #V2 | #I2 #L2 ] #n #HL #g1a #Hg1a #g2 #Hg2
  32     lapply (Hn n) -Hn <Hg1a -Hg1a #H
  33     elim (sor_nxx_tl … H) -H /2 width=5 by/
  34   | @sle_xn_tl [2: |*: // ]
  35     @IHb -IHa -IHb [| #I2 #L2 #V2 | #I2 #L2 ] * [1,3,5: |*: #n ] #HL #g1b #Hg1b #g2 #Hg2
  36     [1,2,3:
  37       lapply (drops_fwd_isid … HL ?) -HL // #H destruct -H1 -H2 -H3
  38       /3 width=5 by sle_isid_sn, sle_next/
  39     |4,5,6:
  40       lapply (drops_inv_drop1 … HL) -HL #HL
  41       lapply (Hn n) -Hn >tls_xn <Hg1b -Hg1b #H
  42       elim (sor_xnx_tl … H) -H /3 width=5 by sle_weak/
  43     ]
  44   ]
  45 | #f1a #f1b #f1 #I1 #L1 #V1 #T1 #_ #_ #Hf1 #IHa #IHb #f2 #H1 #H2 #H3
  46   lapply (sor_tls … Hf1) #H
  47   @(sor_inv_sle … Hf1) -Hf1
  48   [ @IHa -IHa -IHb [| #I2 #L2 #V2 | #I2 #L2 ] #n #HL #g1a #Hg1a #g2 #Hg2
  49     lapply (H n) -H <Hg1a -Hg1a #H
  50     elim (sor_nxx_tl … H) -H /2 width=5 by/
  51   | @IHb -IHa -IHb [| #I2 #L2 #V2 | #I2 #L2 ] #n #HL #g1b #Hg1b #g2 #Hg2
  52     lapply (H n) -H <Hg1b -Hg1b #H
  53     elim (sor_xnx_tl … H) -H /2 width=5 by/
  54   ]
  55 ]
  56 qed-.