feat(model_theory/syntax): Free variables (#13529)
Defines `term.var_finset` and `bounded_formula.free_var_finset` to consist of all (free) variables used in a term or formula.
Defines `term.restrict_var` and `bounded_formula.restrict_free_var` to restrict formulas to sets of their variables.
