∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀b,f,L0. ⬇*[b, f] L0 ≡ L1 →
∀T0. ⬆*[f] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
⦃G, L2, T0⦄ ϵ[RP] 〚A〛.
∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀b,f,L0. ⬇*[b, f] L0 ≡ L1 →
∀T0. ⬆*[f] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
⦃G, L2, T0⦄ ϵ[RP] 〚A〛.
#Z #Y #X #IH #G #L1 * [ * | * [ #p ] * ]
[ #s #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct -IH
lapply (aaa_inv_sort … HA) -HA #H destruct
#Z #Y #X #IH #G #L1 * [ * | * [ #p ] * ]
[ #s #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct -IH
lapply (aaa_inv_sort … HA) -HA #H destruct
lapply (drops_trans … HL01 … HLK1 ??) -HL01 [3: |*: // ] #H
elim (drops_split_trans … H) -H [ |*: /2 width=6 by after_uni_dx/ ] #Y #HLK0 #HY
lapply (drops_tls_at … Hf … HY) -Hf -HY #HY
lapply (drops_trans … HL01 … HLK1 ??) -HL01 [3: |*: // ] #H
elim (drops_split_trans … H) -H [ |*: /2 width=6 by after_uni_dx/ ] #Y #HLK0 #HY
lapply (drops_tls_at … Hf … HY) -Hf -HY #HY
elim (lifts_total V0 (𝐔❴⫯j❵)) #V #HV0
elim (lsubc_drops_trans_isuni … HL20 … HLK0) -HL20 -HLK0 // #Y #HLK2 #H
elim (lifts_total V0 (𝐔❴⫯j❵)) #V #HV0
elim (lsubc_drops_trans_isuni … HL20 … HLK0) -HL20 -HLK0 // #Y #HLK2 #H
[ #K2 #HK20 #H destruct
lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b
lapply (s5 … HA ? G ? ? (◊) … HV0 ?) -HA
/4 width=11 by acr_lifts, fqup_lref, drops_inv_gen/
[ #K2 #HK20 #H destruct
lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b
lapply (s5 … HA ? G ? ? (◊) … HV0 ?) -HA
/4 width=11 by acr_lifts, fqup_lref, drops_inv_gen/
lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b
lapply (aaa_lifts … HKV1 … HK01 … HV10) -HKV1 -HK01 -HV10 #HKV0A
lapply (aaa_mono … HKV0B … HKV0A) #H destruct -HKV0B -HKV0A
elim (lifts_total V2 (𝐔❴⫯j❵)) #V3 #HV23
lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b
lapply (aaa_lifts … HKV1 … HK01 … HV10) -HKV1 -HK01 -HV10 #HKV0A
lapply (aaa_mono … HKV0B … HKV0A) #H destruct -HKV0B -HKV0A
elim (lifts_total V2 (𝐔❴⫯j❵)) #V3 #HV23
[3: |*: /2 width=9 by drops_inv_gen, lifts_flat/ ] -HLK2
lapply (s7 … HA G L2 (◊)) -HA /3 width=7 by acr_lifts/
]
[3: |*: /2 width=9 by drops_inv_gen, lifts_flat/ ] -HLK2
lapply (s7 … HA G L2 (◊)) -HA /3 width=7 by acr_lifts/
]
- lapply (s6 … HA G L2 (◊) (◊)) /4 width=10 by lsubc_pair, liftsv_nil, drops_skip/
+ lapply (s6 … HA G L2 (◊) (◊)) /5 width=10 by lsubc_bind, liftsv_nil, drops_skip, ext2_pair/
| #W #T #HG #HL #HT #Z0 #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
elim (aaa_inv_abst … HA) -HA #B #A #HW #HT #H destruct
elim (lifts_inv_bind1 … H0) -H0 #W0 #T0 #HW0 #HT0 #H destruct
| #W #T #HG #HL #HT #Z0 #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
elim (aaa_inv_abst … HA) -HA #B #A #HW #HT #H destruct
elim (lifts_inv_bind1 … H0) -H0 #W0 #T0 #HW0 #HT0 #H destruct
lapply (aaa_lifts … HW … (f3∘f) L2 … W3 ?) -HW
[4: |*: /2 width=8 by drops_trans, lifts_trans/ ] #HW3
@(IH … ((↑f3)∘↑f) … (L2. ⓛW3)) -IH
lapply (aaa_lifts … HW … (f3∘f) L2 … W3 ?) -HW
[4: |*: /2 width=8 by drops_trans, lifts_trans/ ] #HW3
@(IH … ((↑f3)∘↑f) … (L2. ⓛW3)) -IH
- /3 width=12 by lsubc_beta, drops_trans, drops_skip, lifts_trans/
+ /4 width=12 by lsubc_beta, drops_trans, drops_skip, lifts_trans, ext2_pair/
| #V #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
elim (aaa_inv_appl … HA) -HA #B #HV #HT
elim (lifts_inv_flat1 … H0) -H0 #V0 #T0 #HV0 #HT0 #H destruct
| #V #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
elim (aaa_inv_appl … HA) -HA #B #HV #HT
elim (lifts_inv_flat1 … H0) -H0 #V0 #T0 #HV0 #HT0 #H destruct