Function minitt::check::expr::check_telescoped

pub fn check_telescoped(
    index: u32, 
    tcs: TCS, 
    first: Typed, 
    second: Expression
) -> TCM<(Level, TCS)>

$$ \frac{\rho,\Gamma\vdash_l A \quad \Gamma\vdash p:⟦A⟧\rho=[\textsf{x}_l]\Rightarrow\Gamma_1 \quad (\rho,p=[\textsf{x}_l]), \Gamma_1\vdash_{l+1}B} {\rho,\Gamma\vdash_l (\Pi /\Sigma) \ p:A.B} $$ To reuse code that checks if a sigma or a pi type is well-typed between check_type and check