feat: Add domains

[RustanLeino]

This PR adds parameterizable domains. A domain declaration as the form

domain DomainName(X, Y) {
  // top-level declarations (domains, types, taggers, functions, axioms, procedures)
}

where DomainName is the name of the domain and X and Y are its type parameters. If there are no type parameters, the parentheses following DomainName can be omitted. In the body of the domain, DomainName, X, and Y are names of types.

To make use of a domain, it must be instantiated. This is done with a declaration of the form

type D = DomainName(t0, t1)

where D names the instantiation and t0 and t1 are types. This declaration declares

• a type D, and
• for every top-level declaration A in the body of DomainName, a declaration named D..A that is a fresh copy of declaration A but replacing the types DomainName, X, and Y with D, t0, and t1, respectively.

There are some limitations in the current design and implementation:

• The types used to instantiate a domain must be types available in the scope before domains have been instantiated.
• There is a missing check to forbid the type of a custom literal from being a type parameter.
• Procedures inside a domain are not yet part of domain instantiation.
• Although a considerable number of pre- and postconditions and invariants have been declared and proved, this PR still contains a few expect statements and assume {:axiom} statements. (The previous assume statements in the resolver have been proven. In particular, in the absence of domains, this PR proves the necessary uniqueness and well-formedness properties of top-level declarations.)
• There are no verification tests for domains.