mathlib

90bd6f54 - feat(model_theory/encoding): A bound on the number of bounded formulas (#13616)

feat(model_theory/encoding): A bound on the number of bounded formulas (#13616) Gives an encoding `first_order.language.bounded_formula.encoding` of bounded formulas as lists. Uses the encoding to bound the number of bounded formulas with `first_order.language.bounded_formula.card_le`.