Function norm_level_le

crates/kernel/src/level.rs:649–664

Semantic `l1 ≤ l2` on canonical forms. For each `(p1, n1)` in `l1`, the contribution `max(n1.const, u_w + v.off for v ∈ n1.var)` in the branch where `p1`'s params are all positive must be dominated by the max of contributions from `{(p2, n_p2) : p2 ⊆ p1}` in the same branch. # Divergence from Lean4Lean Lean4Lean's `NormLevel.le` (`refs/lean4lean/Lean4Lean/Level.lean:164`) looks for a *single* `p

(l1: &NormLevel, l2: &NormLevel)

///   during `normalize_aux` has `v.idx ∈ p2` (so `u_v ≥ 1` in an active
///   branch).
/// - For each `(w, off) ∈ n1.var`, if some `p2 ⊆ p1` has `(w, off') ∈
///   n_p2.var` with `off' ≥ off`, then `l2`'s contribution along active
///   `p1` is at least `u_w + off' ≥ u_w + off`.
///
/// This matches what Lean4Lean's paper-level theory expects but its
/// implementation doesn't cover (cf. the `sorry` on
/// `NormLevel.subsumption_eval` in `Verify/Level.lean:545`, and the absence
/// of any `geq'_wf`).
fn norm_level_le(l1: &NormLevel, l2: &NormLevel) -> bool {
  for (p1, n1) in l1 {
    if n1.constant == 0 && n1.var.is_empty() {
      continue;
    }
    if n1.constant != 0 && !covers_const(l2, p1, n1.constant) {
      return false;
    }
    for v in &n1.var {
      if !covers_var(l2, p1, v.idx, v.offset) {
        return false;