mathlib

6bb8f229 - refactor(model_theory/terms_and_formulas): Improvements to basics of first-order formulas (#12091)

refactor(model_theory/terms_and_formulas): Improvements to basics of first-order formulas (#12091) Improves the simp set of lemmas related to `realize_bounded_formula` and `realize_formula`, so that they simplify higher-level definitions directly, and keep bounded formulas and formulas separate. Generalizes relabelling of bounded formulas. Defines `close_with_exists` and `close_with_forall` to quantify bounded formulas into closed formulas. Defines `bd_iff` and `iff`.