Function univ_eq

crates/kernel/src/level.rs:696–698

Semantic universe equality: `u ≡ v` for all parameter assignments.

(u: &KUniv<M>, v: &KUniv<M>)

/// exact semantic quotient (canonicity §10.6 R5, option (b)).
///
/// `BTreeMap` iteration is key-ordered, so comparing the filtered
/// streams positionally is a sound map comparison.
fn norm_level_eq(l1: &NormLevel, l2: &NormLevel) -> bool {
  let non_empty =
    |&(_, n): &(&Vec<u64>, &Node)| n.constant != 0 || !n.var.is_empty();
  let mut it1 = l1.iter().filter(non_empty);