Commit 2022-03-23 12:35 16fb8e26
View on Github →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.