-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_inv_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
+(* Note: this is used by rex_conf and might be modified *)
+lemma frees_inv_drops_next: ∀f1,L1,T1. L1 ⊢ 𝐅*⦃T1⦄ ≘ f1 →
+ ∀I2,L2,V2,n. ⬇*[n] L1 ≘ L2.ⓑ{I2}V2 →
+ ∀g1. ↑g1 = ⫱*[n] f1 →
+ ∃∃g2. L2 ⊢ 𝐅*⦃V2⦄ ≘ g2 & g2 ⊆ g1.
+#f1 #L1 #T1 #H elim H -f1 -L1 -T1
+[ #f1 #L1 #s #Hf1 #I2 #L2 #V2 #n #_ #g1 #H1 -I2 -L1 -s
+ lapply (isid_tls n … Hf1) -Hf1 <H1 -f1 #Hf1
+ elim (isid_inv_next … Hf1) -Hf1 //
+| #f1 #i #_ #I2 #L2 #V2 #n #H
+ elim (drops_inv_atom1 … H) -H #H destruct
+| #f1 #I1 #L1 #V1 #Hf1 #IH #I2 #L2 #V2 *
+ [ -IH #HL12 lapply (drops_fwd_isid … HL12 ?) -HL12 //
+ #H destruct #g1 #Hgf1 >(injective_next … Hgf1) -g1
+ /2 width=3 by ex2_intro/
+ | -Hf1 #n #HL12 lapply (drops_inv_drop1 … HL12) -HL12
+ #HL12 #g1 <tls_xn <tl_next_rew #Hgf1 elim (IH … HL12 … Hgf1) -IH -HL12 -Hgf1
+ /2 width=3 by ex2_intro/
+ ]
+| #f1 #I1 #L1 #Hf1 #I2 #L2 #V2 *
+ [ #HL12 lapply (drops_fwd_isid … HL12 ?) -HL12 // #H destruct
+ | #n #_ #g1 #Hgf1 elim (isid_inv_next … Hgf1) -Hgf1 <tls_xn /2 width=1 by isid_tls/
+ ]
+| #f1 #I1 #L1 #i #_ #IH #I2 #L2 #V2 *
+ [ -IH #_ #g1 #Hgf1 elim (discr_next_push … Hgf1)
+ | #n #HL12 lapply (drops_inv_drop1 … HL12) -HL12
+ #HL12 #g1 <tls_xn #Hgf1 elim (IH … HL12 … Hgf1) -IH -HL12 -Hgf1
+ /2 width=3 by ex2_intro/