proposition: Lemma vars_ren f x s: x ∈ vars (ren f s) -> exists y, x = f y /\ y ∈ vars s.
proof: Proof. intros; edestruct varof_ren as [y]; [|exists y]; intuition; eauto. Qed.
imports: List Lia Undecidability.HOU(calculus.terms calculus.prelim std.std)