include "basic_2/static/frees_drops.ma".

axiom frees_inv_drops_next_sle: ∀f1,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → ∀f2. f1 ⊆ f2 →
                                ∀I2,L2,V2,n. ⬇*[n] L1 ≡ L2.ⓑ{I2}V2 →
                                ∀g1. ⫯g1 = ⫱*[n] f1 →
                                ∀g2. L2 ⊢ 𝐅*⦃V2⦄ ≡ g2 → ↑*[n]⫯g2 ⊆ f2.

lemma frees_drops_next_sle: ∀f1,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → ∀f2. (
                               ∀n. ⬇*[Ⓕ, 𝐔❴n❵] L1 ≡ ⋆ →
                               ∀g1. ⫯g1 = ⫱*[n] f1 →
                               ∀g2. 𝐈⦃g2⦄ → ↑*[n]⫯g2 ⊆ f2
                            ) → (
                               ∀I2,L2,V2,n. ⬇*[n] L1 ≡ L2.ⓑ{I2}V2 →
                               ∀g1. ⫯g1 = ⫱*[n] f1 →
                               ∀g2. L2 ⊢ 𝐅*⦃V2⦄ ≡ g2 → ↑*[n]⫯g2 ⊆ f2
                            ) → (
                               ∀I2,L2,n. ⬇*[n] L1 ≡ L2.ⓤ{I2} →
                               ∀g1. ⫯g1 = ⫱*[n] f1 →
                               ∀g2. 𝐈⦃g2⦄ → ↑*[n]⫯g2 ⊆ f2
                            ) → f1 ⊆ f2.
#f1 #L1 #T1 #H @(frees_ind_void … H) -f1 -L1 -T1
[ /2 width=1 by sle_isid_sn/
| /2 width=2 by/
| /3 width=5 by drops_refl/
| /3 width=3 by drops_refl/
| /6 width=5 by drops_drop, sle_inv_tl_dx, sle_px_tl/
| /2 width=1 by sle_isid_sn/
| #f1a #f1b #f1 #p #I1 #L1 #V1 #T1 #_ #_ #Hf1 #IHa #IHb #f2 #H1 #H2 #H3
  lapply (sor_tls … Hf1) #Hn
  @(sor_inv_sle … Hf1) -Hf1
  [ @IHa -IHa -IHb [| #I2 #L2 #V2 | #I2 #L2 ] #n #HL #g1a #Hg1a #g2 #Hg2
    lapply (Hn n) -Hn <Hg1a -Hg1a #H
    elim (sor_nxx_tl … H) -H /2 width=5 by/
  | @sle_xn_tl [2: |*: // ]
    @IHb -IHa -IHb [| #I2 #L2 #V2 | #I2 #L2 ] * [1,3,5: |*: #n ] #HL #g1b #Hg1b #g2 #Hg2
    [1,2,3:
      lapply (drops_fwd_isid … HL ?) -HL // #H destruct -H1 -H2 -H3
      /3 width=5 by sle_isid_sn, sle_next/
    |4,5,6:
      lapply (drops_inv_drop1 … HL) -HL #HL
      lapply (Hn n) -Hn >tls_xn <Hg1b -Hg1b #H
      elim (sor_xnx_tl … H) -H /3 width=5 by sle_weak/
    ]
  ]
| #f1a #f1b #f1 #I1 #L1 #V1 #T1 #_ #_ #Hf1 #IHa #IHb #f2 #H1 #H2 #H3
  lapply (sor_tls … Hf1) #H
  @(sor_inv_sle … Hf1) -Hf1
  [ @IHa -IHa -IHb [| #I2 #L2 #V2 | #I2 #L2 ] #n #HL #g1a #Hg1a #g2 #Hg2
    lapply (H n) -H <Hg1a -Hg1a #H
    elim (sor_nxx_tl … H) -H /2 width=5 by/
  | @IHb -IHa -IHb [| #I2 #L2 #V2 | #I2 #L2 ] #n #HL #g1b #Hg1b #g2 #Hg2
    lapply (H n) -H <Hg1b -Hg1b #H
    elim (sor_xnx_tl … H) -H /2 width=5 by/
  ]
]
qed-.