Function normalize_instance_term 

pub fn normalize_instance_term(
    toplevel: &Toplevel,
    th: &TheoryDef,
    inst: &Instance,
    tm: &FiberTmV,
    over: &BaseTmV,
) -> Result<NormalizedInstanceTerm, String>

Normalizes a single already-elaborated fiber term tm (lying over the codomain object over) in the context of the instance inst, returning its flat normal form.

This is what backs norm [inst] <term>: the term is elaborated against inst’s fiber scope elsewhere (in text_elab), then handed here to run the same extraction that turns an instance body’s equations into modal::ModalInstanceTerms — which is where nested morphism applications get composed into a single (Composite/List) morphism.