Commit 2022-02-22 20:21 6bb8f229
View on Github →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.