mathlib3

260d5ced - feat(model_theory/semantics): Realizing restricted terms and formulas (#14014)

feat(model_theory/semantics): Realizing restricted terms and formulas (#14014) Shows that realizing a restricted term or formula gives the same value as the unrestricted version.