Function minitt::check::expr::check_sum_type

pub fn check_sum_type(
    index: u32, 
    tcs: TCS, 
    constructors: Branch
) -> TCM<(Level, TCS)>

$$ \frac{\rho,\Gamma\vdash_l A_1\Leftarrow \textsf{U} \dots \rho,\Gamma\vdash_l A_n\Leftarrow \textsf{U}} {\rho,\Gamma\vdash_l \textsf{Sum}(c_1\ A_1|\dots|c_n\ A_n)\Leftarrow \textsf{U}} $$ To reuse code that checks if a sum type is well-typed between check_type and check