1 include "basic_2/static/frees_drops.ma".
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.
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
13 āI2,L2,V2,n. ā¬*[n] L1 ā” L2.ā{I2}V2 ā
14 āg1. ā«Æg1 = ā«±*[n] f1 ā
15 āg2. L2 ā¢ š
*ā¦V2ā¦ ā” g2 ā ā*[n]ā«Æg2 ā f2
17 āI2,L2,n. ā¬*[n] L1 ā” L2.ā¤{I2} ā
18 āg1. ā«Æg1 = ā«±*[n] f1 ā
19 āg2. šā¦g2ā¦ ā ā*[n]ā«Æg2 ā f2
21 #f1 #L1 #T1 #H @(frees_ind_void ā¦ H) -f1 -L1 -T1
22 [ /2 width=1 by sle_isid_sn/
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
37 lapply (drops_fwd_isid ā¦ HL ?) -HL // #H destruct -H1 -H2 -H3
38 /3 width=5 by sle_isid_sn, sle_next/
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/
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/