Function resolve_const_levels 

pub fn resolve_const_levels(
    name: &str,
    declared: Option<&[String]>,
    ty: &Term,
    levels: &[Universe],
) -> Result<HashMap<String, Universe>, ConstError>

Resolve a Term::Const { name, levels } against a declaration, producing the universe substitution to apply to its type AND its body (rules 1-3 above). This is the ONE place the decision is made; instantiate_universes applies the result.