mathlib3

13e08bf3 - feat(model_theory/*): Constructors for low-arity languages and structures (#12960)

feat(model_theory/*): Constructors for low-arity languages and structures (#12960) Defines `first_order.language.mk₂` to make it easier to define a language with at-most-binary symbols. Defines `first_order.language.Structure.mk₂` to make it easier to define a structure in a language defined with `first_order.language₂`. Defines `first_order.language.functions.apply₁` and `first_order.language.functions.apply₂` to make it easier to construct terms using low-arity function symbols. Defines `first_order.language.relations.formula₁` and `first_order.language.relations.formula₂` to make it easier to construct formulas using low-arity relation symbols.