(* 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 →
(* 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 →