Function instantiate_universes 

pub fn instantiate_universes(
    term: &Term,
    subst: &HashMap<String, Universe>,
) -> Term

Instantiate universe variables throughout a term: substitute every Sort’s level by subst. This specializes a universe-POLYMORPHIC term (λA:Sort u. …) to a concrete level (u := Type 0), yielding an ordinary term the kernel checks as-is — so one definition is reused at every level instead of duplicated.