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