chore(model_theory/terms_and_formulas): `realize_to_prenex` (#12884)
chore(model_theory/terms_and_formulas): `realize_to_prenex` (#12884)

Proves that `phi.to_prenex` has the same realization in a nonempty structure as the original formula `phi` directly, rather than using `semantically_equivalent`.





leanprover-community/mathlib,leanprover-community/mathlib