(**************************************************************************)
include "ground_2/relocation/rtmap_pushs.ma".
-include "basic_2/relocation/drops.ma".
+include "ground_2/relocation/rtmap_coafter.ma".
+include "basic_2/relocation/drops_drops.ma".
include "basic_2/static/frees.ma".
(* CONTEXT-SENSITIVE FREE VARIABLES *****************************************)
(* Advanced properties ******************************************************)
-lemma drops_atom_F: ∀f. ⬇*[Ⓕ, f] ⋆ ≡ ⋆.
-#f @drops_atom #H destruct
+lemma frees_lref_atom: ∀b,L,i. ⬇*[b, 𝐔❴i❵] L ≡ ⋆ →
+ ∀f. 𝐈⦃f⦄ → L ⊢ 𝐅*⦃#i⦄ ≡ f.
+#b #L elim L -L /2 width=1 by frees_atom/
+#L #I #V #IH *
+[ #H lapply (drops_fwd_isid … H ?) -H // #H destruct
+| /5 width=3 by frees_eq_repl_back, frees_lref, drops_inv_drop1, eq_push_inv_isid/
+]
qed.
+lemma frees_lref_pair: ∀f,K,V. K ⊢ 𝐅*⦃V⦄ ≡ f →
+ ∀i,I,L. ⬇*[i] L ≡ K.ⓑ{I}V → L ⊢ 𝐅*⦃#i⦄ ≡ ↑*[i] ⫯f.
+#f #K #V #Hf #i elim i -i
+[ #I #L #H lapply (drops_fwd_isid … H ?) -H /2 width=1 by frees_zero/
+| #i #IH #I #L #H elim (drops_inv_succ … H) -H /3 width=2 by frees_lref/
+]
+qed.
+
+(* Advanced inversion lemmas ************************************************)
+
lemma frees_inv_lref_drops: ∀i,f,L. L ⊢ 𝐅*⦃#i⦄ ≡ f →
(⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ ∧ 𝐈⦃f⦄) ∨
∃∃g,I,K,V. K ⊢ 𝐅*⦃V⦄ ≡ g &
]
qed-.
+(* Properties with generic slicing for local environments *******************)
-
-lemma frees_dec: ∀L,U,l,i. Decidable (frees l L U i).
-#L #U @(f2_ind … rfw … L U) -L -U
-#x #IH #L * *
-[ -IH /3 width=5 by frees_inv_sort, or_intror/
-| #j #Hx #l #i elim (ylt_split_eq i j) #Hji
- [ -x @or_intror #H elim (ylt_yle_false … Hji)
- lapply (frees_inv_lref_ge … H ?) -L -l /2 width=1 by ylt_fwd_le/
- | -x /2 width=1 by or_introl/
- | elim (ylt_split j l) #Hli
- [ -x @or_intror #H elim (ylt_yle_false … Hji)
- lapply (frees_inv_lref_skip … H ?) -L //
- | elim (lt_or_ge j (|L|)) #Hj
- [ elim (drop_O1_lt (Ⓕ) L j) // -Hj #I #K #W #HLK destruct
- elim (IH K W … 0 (i-j-1)) -IH [1,3: /3 width=5 by frees_lref_be, drop_fwd_rfw, or_introl/ ] #HnW
- @or_intror #H elim (frees_inv_lref_lt … H) // #Z #Y #X #_ #HLY -l
- lapply (drop_mono … HLY … HLK) -L #H destruct /2 width=1 by/
- | -x @or_intror #H elim (ylt_yle_false … Hji)
- lapply (frees_inv_lref_free … H ?) -l //
- ]
- ]
- ]
-| -IH /3 width=5 by frees_inv_gref, or_intror/
-| #a #I #W #U #Hx #l #i destruct
- elim (IH L W … l i) [1,3: /3 width=1 by frees_bind_sn, or_introl/ ] #HnW
- elim (IH (L.ⓑ{I}W) U … (⫯l) (i+1)) -IH [1,3: /3 width=1 by frees_bind_dx, or_introl/ ] #HnU
- @or_intror #H elim (frees_inv_bind … H) -H /2 width=1 by/
-| #I #W #U #Hx #l #i destruct
- elim (IH L W … l i) [1,3: /3 width=1 by frees_flat_sn, or_introl/ ] #HnW
- elim (IH L U … l i) -IH [1,3: /3 width=1 by frees_flat_dx, or_introl/ ] #HnU
- @or_intror #H elim (frees_inv_flat … H) -H /2 width=1 by/
-]
-qed-.
-
-lemma frees_S: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[yinj l]⦃U⦄ → ∀I,K,W. ⬇[l] L ≡ K.ⓑ{I}W →
- (K ⊢ ⫰(i-l) ϵ 𝐅*[0]⦃W⦄ → ⊥) → L ⊢ i ϵ 𝐅*[⫯l]⦃U⦄.
-#L #U #l #i #H elim (frees_inv … H) -H /3 width=2 by frees_eq/
-* #I #K #W #j #Hlj #Hji #HnU #HLK #HW #I0 #K0 #W0 #HLK0 #HnW0
-lapply (yle_inv_inj … Hlj) -Hlj #Hlj
-elim (le_to_or_lt_eq … Hlj) -Hlj
-[ -I0 -K0 -W0 /3 width=9 by frees_be, yle_inj/
-| -Hji -HnU #H destruct
- lapply (drop_mono … HLK0 … HLK) #H destruct -I
- elim HnW0 -L -U -HnW0 //
-]
+axiom coafter_inv_xpx: ∀g2,f1,g. g2 ~⊚ ↑f1 ≡ g → ∀n. @⦃0, g2⦄ ≡ n →
+ ∃∃f2,f. f2 ~⊚ f1 ≡ f & ⫱*[n]g2 = ↑f2 & ⫱*[n]g = ↑f.
+(*
+#g2 #g1 #g #Hg #n #Hg2
+lapply (coafter_tls … Hg2 … Hg) -Hg #Hg
+lapply (at_pxx_tls … Hg2) -Hg2 #H
+elim (at_inv_pxp … H) -H [ |*: // ] #f2 #H2
+elim (coafter_inv_pxx … Hg … H2) -Hg * #f1 #f #Hf #H1 #H0 destruct
+<tls_rew_S <tls_rew_S <H2 <H0 -g2 -g -n //
qed.
+*)
-(* Note: lemma 1250 *)
-lemma frees_bind_dx_O: ∀a,I,L,W,U,i. L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[0]⦃U⦄ →
- L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄.
-#a #I #L #W #U #i #HU elim (frees_dec L W 0 i)
-/4 width=5 by frees_S, frees_bind_dx, frees_bind_sn/
+lemma coafter_tls_succ: ∀g2,g1,g. g2 ~⊚ g1 ≡ g →
+ ∀n. @⦃0, g2⦄ ≡ n → ⫱*[⫯n]g2 ~⊚ ⫱g1 ≡ ⫱*[⫯n]g.
+#g2 #g1 #g #Hg #n #Hg2
+lapply (coafter_tls … Hg2 … Hg) -Hg #Hg
+lapply (at_pxx_tls … Hg2) -Hg2 #H
+elim (at_inv_pxp … H) -H [ |*: // ] #f2 #H2
+elim (coafter_inv_pxx … Hg … H2) -Hg * #f1 #f #Hf #H1 #H0 destruct
+<tls_rew_S <tls_rew_S <H2 <H0 -g2 -g -n //
qed.
-(* Properties on relocation *************************************************)
-
-lemma frees_lift_ge: ∀K,T,l,i. K ⊢ i ϵ𝐅*[l]⦃T⦄ →
- ∀L,s,l0,m0. ⬇[s, l0, m0] L ≡ K →
- ∀U. ⬆[l0, m0] T ≡ U → l0 ≤ i →
- L ⊢ i+m0 ϵ 𝐅*[l]⦃U⦄.
-#K #T #l #i #H elim H -K -T -l -i
-[ #K #T #l #i #HnT #L #s #l0 #m0 #_ #U #HTU #Hl0i -K -s
- @frees_eq #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
-| #I #K #K0 #T #V #l #i #j #Hlj #Hji #HnT #HK0 #HV #IHV #L #s #l0 #m0 #HLK #U #HTU #Hl0i
- elim (ylt_split j l0) #H0
- [ elim (drop_trans_lt … HLK … HK0) // -K #L0 #W #HL0 >yminus_SO2 #HLK0 #HVW
- @(frees_be … HL0) -HL0 -HV /3 width=3 by ylt_plus_dx2_trans/
- [ lapply (ylt_fwd_lt_O1 … H0) #H1
- #X #HXU <(ymax_pre_sn l0 1) in HTU; /2 width=1 by ylt_fwd_le_succ1/ #HTU
- <(ylt_inv_O1 l0) in H0; // -H1 #H0
- elim (lift_div_le … HXU … HTU ?) -U /2 width=2 by ylt_fwd_succ2/
- | >yplus_minus_comm_inj /2 width=1 by ylt_fwd_le/
- <yplus_pred1 /4 width=5 by monotonic_yle_minus_dx, yle_pred, ylt_to_minus/
- ]
- | lapply (drop_trans_ge … HLK … HK0 ?) // -K #HLK0
- lapply (drop_inv_gen … HLK0) >commutative_plus -HLK0 #HLK0
- @(frees_be … HLK0) -HLK0 -IHV
- /2 width=1 by monotonic_ylt_plus_dx, yle_plus_dx1_trans/
- [ #X <yplus_inj #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
- | <yplus_minus_assoc_comm_inj //
- ]
- ]
+lemma frees_lifts: ∀b,f1,K,T. K ⊢ 𝐅*⦃T⦄ ≡ f1 →
+ ∀f,L. ⬇*[b, f] L ≡ K → ∀U. ⬆*[f] T ≡ U →
+ ∀f2. f ~⊚ f1 ≡ f2 → L ⊢ 𝐅*⦃U⦄ ≡ f2.
+#b #f1 #K #T #H lapply (frees_fwd_isfin … H) elim H -f1 -K -T
+[ #f1 #I #Hf1 #_ #f #L #H1 #U #H2 #f2 #H3
+ lapply (coafter_isid_inv_dx … H3 … Hf1) -f1 #Hf2
+ elim (lifts_inv_atom1 … H2) -H2 *
+ /2 width=1 by frees_sort_gen, frees_gref_gen/
+ #i #j #Hij #H #H0 destruct
+ elim (drops_inv_atom2 … H1) -H1 #n #g #H1 #Hf
+ elim (after_at_fwd … Hij … Hf) -f #x #_ #Hj -g -i
+ lapply (at_inv_uni … Hj) -Hj #H destruct
+ /3 width=8 by frees_lref_atom, drops_trans/
+| #f1 #I #K #V #s #_ #IH #Hf1 #f #L #H1 #U #H2 #f2 #H3
+ lapply (isfin_fwd_push … Hf1 ??) -Hf1 [3: |*: // ] #Hf1
+ lapply (lifts_inv_sort1 … H2) -H2 #H destruct
+ lapply (at_total 0 f) #H
+ elim (drops_split_trans … H1) -H1
+ [5: @(after_uni_dx … H) /2 width=1 by after_isid_dx/ |2,3: skip
+ |4: // ] #X #HLX #HXK
+ lapply (drops_inv_tls_at … H … HXK) -HXK #HXK
+ elim (drops_inv_skip2 … HXK) -HXK
+ #Y #W #HYK #HVW #H0 destruct
+(*
+
+ elim (coafter_inv_xpx … H3 ??) -H3 [ |*: // ] #g2 #g #Hg #H2 #H0
+ lapply (IH … Hg) -IH -Hg
+ [1,5: // | skip
+ |
+ |6: #H
+*)
+
+ lapply (coafter_tls_succ … H3 ??) -H3 [3: |*: // ] #H3
+ lapply (IH … HYK … H3) -IH -H3 -HYK
+ [1,3: // | skip ]
+ #H lapply (frees_sort … H)
+
+ ]
+
+
+ elim (coafter_inv_xxp … H3) -H3 [1,3: * |*: // ]
+ [ #g #g1 #Hf2 #H #H0 destruct
+ elim (drops_inv_skip1 … H1) -H1 #K #V #HLK #_ #H destruct
+ | #g #Hf2 #H destruct
+ lapply (drops_inv_drop1 … H1) -H1
+ ] /3 width=4 by frees_sort/
+
+|
+|
+|
+| #f1V #f1T #f1 #p #I #K #V #T #_ #_ #H1f1 #IHV #IHT #H2f1 #f #L #H1 #Y #H2 #f2 #H3
+ elim (sor_inv_isfin3 … H1f1) // #Hf1V #H
+ lapply (isfin_inv_tl … H) -H
+ elim (lifts_inv_bind1 … H2) -H2 #W #U #HVW #HTU #H destruct
+ elim (coafter_sor … H3 … H1f1) /2 width=5 by coafter_isfin2_fwd/ -H3 -H1f1 #f2V #f2T #Hf2V #H
+ elim (coafter_inv_tl1 … H) -H /4 width=5 by frees_bind, drops_skip/
+| #f1V #f1T #f1 #I #K #V #T #_ #_ #H1f1 #IHV #IHT #H2f1 #f #L #H1 #Y #H2 #f2 #H3
+ elim (sor_inv_isfin3 … H1f1) //
+ elim (lifts_inv_flat1 … H2) -H2 #W #U #HVW #HTU #H destruct
+ elim (coafter_sor … H3 … H1f1)
+ /3 width=5 by coafter_isfin2_fwd, frees_flat/
]
-qed.
-(* Inversion lemmas on relocation *******************************************)
-
-lemma frees_inv_lift_be: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
- ∀K,s,l0,m0. ⬇[s, l0, m0+1] L ≡ K →
- ∀T. ⬆[l0, m0+1] T ≡ U → l0 ≤ i → i ≤ l0 + m0 → ⊥.
-#L #U #l #i #H elim H -L -U -l -i
-[ #L #U #l #i #HnU #K #s #l0 #m0 #_ #T #HTU #Hl0i #Hilm0
- elim (lift_split … HTU i m0) -HTU /2 width=2 by/
-| #I #L #K0 #U #W #l #i #j #Hli #Hij #HnU #HLK0 #_ #IHW #K #s #l0 #m0 #HLK #T #HTU #Hl0i #Hilm0
- elim (ylt_split j l0) #H1
- [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
- @(IHW … HKL0 … HVW)
- [ /3 width=1 by monotonic_yle_minus_dx, yle_pred/
- | >yplus_pred1 /2 width=1 by ylt_to_minus/
- <yplus_minus_comm_inj /3 width=1 by monotonic_yle_minus_dx, yle_pred, ylt_fwd_le/
- ]
- | elim (lift_split … HTU j m0) -HTU /3 width=3 by ylt_yle_trans, ylt_fwd_le/
- ]
+(* Inversion lemmas with generic slicing for local environments *************)
+
+lemma frees_inv_lifts: ∀b,f2,L,U. L ⊢ 𝐅*⦃U⦄ ≡ f2 →
+ ∀f,K. ⬇*[b, f] L ≡ K → ∀T. ⬆*[f] T ≡ U →
+ ∀f1. f ~⊚ f1 ≡ f2 → K ⊢ 𝐅*⦃T⦄ ≡ f1.
+#b #f2 #L #U #H lapply (frees_fwd_isfin … H) elim H -f2 -L -U
+[ #f2 #I #Hf2 #_ #f #K #H1 #T #H2 #f1 #H3
+ lapply (coafter_fwd_isid2 … H3 … Hf2) -H3 // -Hf2 #Hf1
+ elim (drops_inv_atom1 … H1) -H1 #H #_ destruct
+ elim (lifts_inv_atom2 … H2) -H2 * /2 width=3 by frees_atom/
+| #f2 #I #L #W #s #_ #IH #Hf2 #f #Y #H1 #T #H2 #f1 #H3
+ lapply (isfin_fwd_push … Hf2 ??) -Hf2 [3: |*: // ] #Hf2
+ lapply (lifts_inv_sort2 … H2) -H2 #H destruct
+ elim (coafter_inv_xxp … H3) -H3 [1,3: * |*: // ]
+ [ #g #g1 #Hf2 #H #H0 destruct
+ elim (drops_inv_skip1 … H1) -H1 #K #V #HLK #_ #H destruct
+ | #g #Hf2 #H destruct
+ lapply (drops_inv_drop1 … H1) -H1
+ ] /3 width=4 by frees_sort/
+| #f2 #I #L #W #_ #IH #Hf2 #f #Y #H1 #T #H2 #f1 #H3
+ lapply (isfin_inv_next … Hf2 ??) -Hf2 [3: |*: // ] #Hf2
+ elim (lifts_inv_lref2 … H2) -H2 #i #H2 #H destruct
+ lapply (at_inv_xxp … H2 ?) -H2 // * #g #H #H0 destruct
+ elim (drops_inv_skip1 … H1) -H1 #K #V #HLK #HVW #H destruct
+ elim (coafter_inv_pxn … H3) -H3 [ |*: // ] #g1 #Hf2 #H destruct
+ /3 width=4 by frees_zero/
+| #f2 #I #L #W #j #_ #IH #Hf2 #f #Y #H1 #T #H2 #f1 #H3
+ lapply (isfin_fwd_push … Hf2 ??) -Hf2 [3: |*: // ] #Hf2
+ elim (lifts_inv_lref2 … H2) -H2 #x #H2 #H destruct
+ elim (coafter_inv_xxp … H3) -H3 [1,3: * |*: // ]
+ [ #g #g1 #Hf2 #H #H0 destruct
+ elim (drops_inv_skip1 … H1) -H1 #K #V #HLK #HVW #H destruct
+ elim (at_inv_xpn … H2) -H2 [ |*: // ] #j #Hg #H destruct
+ | #g #Hf2 #H destruct
+ lapply (drops_inv_drop1 … H1) -H1
+ lapply (at_inv_xnn … H2 ????) -H2 [5: |*: // ]
+ ] /4 width=4 by lifts_lref, frees_lref/
+| #f2 #I #L #W #l #_ #IH #Hf2 #f #Y #H1 #T #H2 #f1 #H3
+ lapply (isfin_fwd_push … Hf2 ??) -Hf2 [3: |*: // ] #Hf2
+ lapply (lifts_inv_gref2 … H2) -H2 #H destruct
+ elim (coafter_inv_xxp … H3) -H3 [1,3: * |*: // ]
+ [ #g #g1 #Hf2 #H #H0 destruct
+ elim (drops_inv_skip1 … H1) -H1 #K #V #HLK #_ #H destruct
+ | #g #Hf2 #H destruct
+ lapply (drops_inv_drop1 … H1) -H1
+ ] /3 width=4 by frees_gref/
+| #f2W #f2U #f2 #p #I #L #W #U #_ #_ #H1f2 #IHW #IHU #H2f2 #f #K #H1 #X #H2 #f1 #H3
+ elim (sor_inv_isfin3 … H1f2) // #H1f2W #H
+ lapply (isfin_inv_tl … H) -H
+ elim (lifts_inv_bind2 … H2) -H2 #V #T #HVW #HTU #H destruct
+ elim (coafter_inv_sor … H3 … H1f2) -H3 -H1f2 // #f1W #f1U #H2f2W #H
+ elim (coafter_inv_tl0 … H) -H /4 width=5 by frees_bind, drops_skip/
+| #f2W #f2U #f2 #I #L #W #U #_ #_ #H1f2 #IHW #IHU #H2f2 #f #K #H1 #X #H2 #f1 #H3
+ elim (sor_inv_isfin3 … H1f2) //
+ elim (lifts_inv_flat2 … H2) -H2 #V #T #HVW #HTU #H destruct
+ elim (coafter_inv_sor … H3 … H1f2) -H3 -H1f2 /3 width=5 by frees_flat/
]
qed-.
-lemma frees_inv_lift_ge: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
- ∀K,s,l0,m0. ⬇[s, l0, m0] L ≡ K →
- ∀T. ⬆[l0, m0] T ≡ U → l0 + m0 ≤ i →
- K ⊢ i-m0 ϵ𝐅*[l-yinj m0]⦃T⦄.
-#L #U #l #i #H elim H -L -U -l -i
-[ #L #U #l #i #HnU #K #s #l0 #m0 #HLK #T #HTU #Hlm0i -L -s
- elim (yle_inv_plus_inj2 … Hlm0i) -Hlm0i #Hl0im0 #Hm0i @frees_eq #X #HXT -K
- elim (lift_trans_le … HXT … HTU) -T // >ymax_pre_sn /2 width=2 by/
-| #I #L #K0 #U #W #l #i #j #Hli #Hij #HnU #HLK0 #_ #IHW #K #s #l0 #m0 #HLK #T #HTU #Hlm0i
- elim (ylt_split j l0) #H1
- [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
- elim (yle_inv_plus_inj2 … Hlm0i) #H0 #Hm0i
- @(frees_be … H) -H
- [ /3 width=1 by yle_plus_dx1_trans, monotonic_yle_minus_dx/
- | /2 width=3 by ylt_yle_trans/
- | #X #HXT elim (lift_trans_ge … HXT … HTU) -T /2 width=2 by ylt_fwd_le_succ1/
- | lapply (IHW … HKL0 … HVW ?) // -I -K -K0 -L0 -V -W -T -U -s
- >yplus_pred1 /2 width=1 by ylt_to_minus/
- <yplus_minus_comm_inj /3 width=1 by monotonic_yle_minus_dx, yle_pred, ylt_fwd_le/
- ]
- | elim (ylt_split j (l0+m0)) #H2
- [ -L -I -W elim (yle_inv_inj2 … H1) -H1 #x #H1 #H destruct
- lapply (ylt_plus2_to_minus_inj1 … H2) /2 width=1 by yle_inj/ #H3
- lapply (ylt_fwd_lt_O1 … H3) -H3 #H3
- elim (lift_split … HTU j (m0-1)) -HTU /2 width=1 by yle_inj/
- [ >minus_minus_associative /2 width=1 by ylt_inv_inj/ <minus_n_n
- -H2 #X #_ #H elim (HnU … H)
- | <yminus_inj >yminus_SO2 >yplus_pred2 /2 width=1 by ylt_fwd_le_pred2/
- ]
- | lapply (drop_conf_ge … HLK … HLK0 ?) // -L #HK0
- elim ( yle_inv_plus_inj2 … H2) -H2 #H2 #Hm0j
- @(frees_be … HK0)
- [ /2 width=1 by monotonic_yle_minus_dx/
- | /2 width=1 by monotonic_ylt_minus_dx/
- | #X #HXT elim (lift_trans_le … HXT … HTU) -T //
- <yminus_inj >ymax_pre_sn /2 width=2 by/
- | <yminus_inj >yplus_minus_assoc_comm_inj //
- >ymax_pre_sn /3 width=5 by yle_trans, ylt_fwd_le/
- ]
- ]
+lemma frees_inv_drops: ∀f2,L,U. L ⊢ 𝐅*⦃U⦄ ≡ f2 →
+ ∀f,K. ⬇*[Ⓣ, f] L ≡ K → ∀f1. f ~⊚ f1 ≡ f2 →
+ ∃∃T. K ⊢ 𝐅*⦃T⦄ ≡ f1 & ⬆*[f] T ≡ U.
+#f2 #L #U #H lapply (frees_fwd_isfin … H) elim H -f2 -L -U
+[ #f2 #I #Hf2 #_ #f #K #H1 #f1 #H2
+ lapply (coafter_fwd_isid2 … H2 ??) -H2 // -Hf2 #Hf1
+ elim (drops_inv_atom1 … H1) -H1 #H #Hf destruct
+ /4 width=3 by frees_atom, lifts_refl, ex2_intro/
+| #f2 #I #L #W #s #_ #IH #Hf2 #f #Y #H1 #f1 #H2
+ lapply (isfin_fwd_push … Hf2 ??) -Hf2 [3: |*: // ] #Hf2
+ elim (coafter_inv_xxp … H2) -H2 [1,3: * |*: // ]
+ [ #g #g1 #Hf2 #H #H0 destruct
+ elim (drops_inv_skip1 … H1) -H1 #K #V #HLK #_ #H destruct
+ | #g #Hf2 #H destruct
+ lapply (drops_inv_drop1 … H1) -H1 #HLK
+ ]
+ elim (IH … HLK … Hf2) -L // -f2 #X #Hg1 #HX
+ lapply (lifts_inv_sort2 … HX) -HX #H destruct
+ /3 width=3 by frees_sort, lifts_sort, ex2_intro/
+| #f2 #I #L #W #_ #IH #Hf2 #f #Y #H1 #f1 #H2
+ lapply (isfin_inv_next … Hf2 ??) -Hf2 [3: |*: // ] #Hf2
+ elim (coafter_inv_xxn … H2) -H2 [ |*: // ] #g #g1 #Hf2 #H0 #H destruct
+ elim (drops_inv_skip1 … H1) -H1 #K #V #HLK #HVW #H destruct
+ elim (IH … HLK … Hf2) -L // -f2 #X #Hg1 #HX
+ lapply (lifts_inj … HX … HVW) -W #H destruct
+ /3 width=3 by frees_zero, lifts_lref, ex2_intro/
+| #f2 #I #L #W #j #_ #IH #Hf2 #f #Y #H1 #f1 #H2
+ lapply (isfin_fwd_push … Hf2 ??) -Hf2 [3: |*: // ] #Hf2
+ elim (coafter_inv_xxp … H2) -H2 [1,3: * |*: // ]
+ [ #g #g1 #Hf2 #H #H0 destruct
+ elim (drops_inv_skip1 … H1) -H1 #K #V #HLK #_ #H destruct
+ | #g #Hf2 #H destruct
+ lapply (drops_inv_drop1 … H1) -H1 #HLK
+ ]
+ elim (IH … HLK … Hf2) -L // -f2 #X #Hg1 #HX
+ elim (lifts_inv_lref2 … HX) -HX #i #Hij #H destruct
+ /4 width=7 by frees_lref, lifts_lref, at_S1, at_next, ex2_intro/
+| #f2 #I #L #W #l #_ #IH #Hf2 #f #Y #H1 #f1 #H2
+ lapply (isfin_fwd_push … Hf2 ??) -Hf2 [3: |*: // ] #Hf2
+ elim (coafter_inv_xxp … H2) -H2 [1,3: * |*: // ]
+ [ #g #g1 #Hf2 #H #H0 destruct
+ elim (drops_inv_skip1 … H1) -H1 #K #V #HLK #_ #H destruct
+ | #g #Hf2 #H destruct
+ lapply (drops_inv_drop1 … H1) -H1 #HLK
]
+ elim (IH … HLK … Hf2) -L // -f2 #X #Hg1 #HX
+ lapply (lifts_inv_gref2 … HX) -HX #H destruct
+ /3 width=3 by frees_gref, lifts_gref, ex2_intro/
+| #f2W #f2U #f2 #p #I #L #W #U #_ #_ #H1f2 #IHW #IHU #H2f2 #f #K #H1 #f1 #H2
+ elim (sor_inv_isfin3 … H1f2) // #H1f2W #H
+ lapply (isfin_inv_tl … H) -H #H1f2U
+ elim (coafter_inv_sor … H2 … H1f2) -H2 -H1f2 // #f1W #f1U #H2f2W #H #Hf1
+ elim (coafter_inv_tl0 … H) -H #g1 #H2f2U #H destruct
+ elim (IHW … H1 … H2f2W) -IHW -H2f2W // -H1f2W #V #Hf1W #HVW
+ elim (IHU … H2f2U) -IHU -H2f2U
+ /3 width=5 by frees_bind, drops_skip, lifts_bind, ex2_intro/
+| #f2W #f2U #f2 #I #L #W #U #_ #_ #H1f2 #IHW #IHU #H2f2 #f #K #H1 #f1 #H2
+ elim (sor_inv_isfin3 … H1f2) // #H1f2W #H1f2U
+ elim (coafter_inv_sor … H2 … H1f2) -H2 -H1f2 // #f1W #f1U #H2f2W #H2f2U #Hf1
+ elim (IHW … H1 … H2f2W) -IHW -H2f2W // -H1f2W
+ elim (IHU … H1 … H2f2U) -L -H2f2U
+ /3 width=5 by frees_flat, lifts_flat, ex2_intro/
]
qed-.