Function minitt::type_check::check_type

pub fn check_type(
    index: u32, 
    context: Telescope, 
    gamma: Gamma, 
    expression: Expression
) -> TCM<()>

checkT in Mini-TT.
Check if an expression is a well-typed type expression.