Function normalize_level

crates/kernel/src/level.rs:687–693

Normalize a universe level to Géran's canonical form.

(l: &KUniv<M>)

/// Entry-wise equality of two normal forms, IGNORING empty entries
/// (constant 0, no vars — pure subsumption bookkeeping). Subsumption
/// EMPTIES a dominated entry rather than removing it, so a spelling like
/// `max (u+1) (imax (u+1) v)` retains an empty `[u,v]` entry that its
/// semantic equal `max (u+1) v` never creates; counting those entries
/// made `univ_eq` strictly finer than semantic equality (3 of 3,253,373
/// whole-Mathlib entries). `norm_level_le` already skips them (see the
/// `continue` guard above); mirroring that here makes `univ_eq` the
/// exact semantic quotient (canonicity §10.6 R5, option (b)).
///
/// `BTreeMap` iteration is key-ordered, so comparing the filtered