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.