]
qed-.
+lemma frees_lifts_SO: ∀b,L,K. ⬇*[b, 𝐔❴1❵] L ≡ K → ∀T,U. ⬆*[1] T ≡ U →
+ ∀f. K ⊢ 𝐅*⦃T⦄ ≡ f → L ⊢ 𝐅*⦃U⦄ ≡ ↑f.
+#b #L #K #HLK #T #U #HTU #f #Hf
+@(frees_lifts b … Hf … HTU) // (**) (* auto fails *)
+qed.
+
(* Forward lemmas with generic slicing for local environments ***************)
lemma frees_fwd_coafter: ∀b,f2,L,U. L ⊢ 𝐅*⦃U⦄ ≡ f2 →
/3 width=7 by frees_eq_repl_back, coafter_inj/
qed-.
+(* Note: this is used by lfxs_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 →