proposition: Lemma consts_subst_vars sigma s: consts (sigma • s) ⊆ consts s ++ Consts (map sigma (vars s)).
proof: Proof. intros x [|[y]] % consts_subst_in; simplify; intuition idtac. right; eapply Consts_consts; eauto using in_map. Qed.
imports: Morphisms Lia List Undecidability.HOU(calculus.calculus)