mathlib3

b24372f6 - feat(model_theory/basic, terms_and_formulas): Helper functions for constant symbols (#12722)

feat(model_theory/basic, terms_and_formulas): Helper functions for constant symbols (#12722) Defines a function `language.con` from `A` to constants of the language `L[[A]]`. Changes the coercion of a constant to a term to a function `language.constants.term`. Proves `simp` lemmas for interpretation of constant symbols and realization of constant terms. Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>