let te = debruijn uri len [] te in
let context,te = NCicReduction.split_prods ~subst tys leftno te in
let _,chopped_context_rev =
let te = debruijn uri len [] te in
let context,te = NCicReduction.split_prods ~subst tys leftno te in
let _,chopped_context_rev =