proposition: Lemma vars_subst_consts x s sigma: x ∈ vars s -> consts (sigma x) ⊆ consts (sigma • s).
proof: Proof. intros H % vars_varof; induction H in sigma |-*; cbn; [auto with listdb..|]. rewrite <-IHvarof; cbn; unfold funcomp; now rewrite consts_ren. Qed.
imports: Morphisms Lia List Undecidability.HOU(calculus.calculus)