Function subsumption

crates/kernel/src/level.rs:549–574

(acc: &mut NormLevel)

      yi += 1;
    }
    if yi >= ys.len() || ys[yi] != x {
      return false;
    }
    yi += 1;
  }
  true
}

fn subsumption(acc: &mut NormLevel) {
  let snapshot: Vec<_> =
    acc.iter().map(|(k, v)| (k.clone(), v.clone())).collect();

  for (p1, n1) in acc.iter_mut() {
    for (p2, n2) in &snapshot {
      if !is_subset(p2, p1) {
        continue;
      }
      let same = p1.len() == p2.len();

      if n1.constant != 0 {
        let max_var_offset = n1.var.iter().map(|v| v.offset).max().unwrap_or(0);
        let keep_const = (same || n1.constant > n2.constant)
          && (n2.var.is_empty() || n1.constant > max_var_offset + 1);
        if !keep_const {
          n1.constant = 0;
        }
      }

      if !same && !n2.var.is_empty() {