The Lean types denoting SMT sorts

The Lean types that sorts denote — sets, bags, total maps, floats, finite-field elements, tuples, relations, records — each with its ToTyp instance and the Lean-side operations it needs. They are shared by both layers. Converting a value to a term and back is done by each theory's module, such as Cvc.Typed.Theory.Set.