Function instance_from_def 

pub fn instance_from_def(
    toplevel: &Toplevel,
    th: &TheoryDef,
    inst: &Instance,
) -> Result<(ModelInstance, Namespace), String>

Generates a ModelInstance from an elaborated Instance declaration.

Walks the instance’s fiber Record, registering each generator with its fiber, each equation as a pair of instance terms, and each sub-instance’s contents under the appropriate prefix.

The codomain model is built with a ModelGenerator, which is then reused to type the instance’s generators and equation terms (this is how modal list modalities are recovered).