Function level_min 

pub fn level_min(l1: &Level, l2: &Level) -> Level

Compute the minimum of two levels: min(l1, l2).

Defined as imax(l1, succ(l2)) is NOT min; instead use: min(l1, l2) = l1 if l1 <= l2, else l2. This is approximate (returns a conservative lower bound for polymorphic levels).