mathlib

1ccb7f04 - feat(model_theory/syntax, semantics): Lemmas about relabeling variables (#14225)

feat(model_theory/syntax, semantics): Lemmas about relabeling variables (#14225) Proves lemmas about relabeling variables in terms and formulas Defines `first_order.language.bounded_formula.to_formula`, which turns turns all of the extra variables of a `bounded_formula` into free variables.