Function univ_geq

crates/kernel/src/level.rs:701–705

Check `u ≥ v` for all parameter assignments.

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

      _ => return false,
    }
  }
}

/// Normalize a universe level to Géran's canonical form.
fn normalize_level<M: KernelMode>(l: &KUniv<M>) -> NormLevel {
  let mut acc = NormLevel::new();
  acc.insert(Vec::new(), Node::default());
  normalize_aux(l, &[], 0, &mut acc);