proposition: Lemma singlepoint_subst_vars x s t: vars (update x s var • t) ⊆ vars s ++ vars t.
proof: Proof. intros ? (y & H1 & H2) % vars_varof % varof_subst. unfold update in *; destruct eq_dec; subst. eapply varof_vars in H2; simplify; eauto. inv H2. eapply varof_vars in H1; simplify; eauto. Qed.
imports: List Lia Arith Init.Wf Morphisms Program.Program Undecidability.HOU(concon.conservativity calculus.calculus) Undecidability.HOU.unification(systemunification nth_order_unification)