Function ordered_insert

crates/kernel/src/level.rs:354–363

Insert into a sorted list, returning `None` if already present.

(a: u64, list: &[u64])

/// Insert `(idx, k)` into the var list at `path`, taking the max of offsets
/// when `idx` is already present. Mirrors Lean4Lean's
/// `NormLevel.addNode v k path'` (`refs/lean4lean/Lean4Lean/Level.lean:92`);
/// `k` must be the current succ-accumulator from `normalize_aux`.
///
/// An earlier port of this function dropped `k` and always inserted
/// `(idx, 0)`, which silently mis-normalized `Succ^n(imax(u, Param v))`
/// shapes for `n > 0`. Keep the `k` parameter.
fn norm_add_node(s: &mut NormLevel, idx: u64, k: u64, path: &[u64]) {
  s.entry(path.to_vec()).or_default().add_var(idx, k);
}

fn norm_add_const(s: &mut NormLevel, k: u64, path: &[u64]) {
  if k == 0 || (k == 1 && !path.is_empty()) {