Polymorphic product type. Eliminate with ``match`` over the single
``mk`` constructor (the generated recursor ``Pair_rec`` is also
available). For SMT-level reasoning about specific projections in
refinements, declare monomorphic uninterpreted helpers per concrete
instantiation, e.g.
def split_fst : (p: (Pair Dataset Dataset)) -> Dataset = uninterpreted
and link them to the runtime values via refined accessors.
For each type in this module: inductive types list their declared constructors; opaque types list any local function whose name starts with mk and which returns a value of that type.