proposition: Lemma singlepoint_subst_vars_variable x s t: x ∈ vars (update x s var • t) -> x ∈ vars s /\ x ∈ vars t.
proof: Proof. intros (y & ? & ?) % vars_varof % varof_subst. unfold update in *; destruct eq_dec; subst; split; eauto using varof_vars. all: now exfalso; inv H0. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)