qed-.
(* 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,i. ⇩[i] L1 ≘ L2.ⓑ[I2]V2 →
qed-.
(* 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,i. ⇩[i] L1 ≘ L2.ⓑ[I2]V2 →