Function minitt::check::decl::check_lift_parameters

pub fn check_lift_parameters<'a>(
    index: u32, 
    tcs: TCS<'a>, 
    parameters: Vec<Typed>, 
    check_body: impl FnOnce(TCS<'a>) -> TCM<LiftState<'a>>
) -> TCM<LiftState<'a>>

$$ \frac{\rho \ \texttt{empty} \quad T:\textsf{U} \quad a:T} {\textnormal{checkLiftD}(a,T,\rho)} $$ $$ \frac{\rho\equiv[(v,T)::\rho'] \quad T:\textsf{U} \quad v:T\vdash R:\textsf{U} \quad \Gamma,v:T\vdash\textnormal{checkLiftD}(a,R,\rho')} {\Gamma\vdash\textnormal{checkLiftD}(\lambda v.a,\Pi (v:T).R,\rho)} $$ This is an extension, it's not present in Mini-TT.
Lift all these parameters into the context.
Returning TCS to reuse the variable.

check_body is supposed to return signature, body and tcs.