Function minitt::check::expr::check_level

pub fn check_level(
    level: u32, 
    (actual_level, tcs): (u32, TCS<'_>)
) -> TCM<TCS<'_>>

$$ \frac{i < j}{\Gamma\vdash \textsf{U}_i <: \textsf{U}_j} $$ Level comparison.