feat(model_theory/basic): Language operations (#12129)
Defines language homomorphisms with `first_order.language.Lhom`
Defines the sum of two languages with `first_order.language.sum`
Defines `first_order.language.with_constants`, a language with added constants, abbreviated `L[[A]]`.
Defines a `L[[A]].Structure` on `M` when `A : set M`.
(Some of this code comes from the Flypitch project)
