mathlib3

715f984a - feat(model_theory/terms_and_formulas): Prenex Normal Form (#12558)

feat(model_theory/terms_and_formulas): Prenex Normal Form (#12558) Defines `first_order.language.bounded_formula.to_prenex`, a function which takes a formula and outputs an equivalent formula in prenex normal form. Proves inductive principles based on the fact that every formula is equivalent to one in prenex normal form.