let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
let params = List.rev_map (function name,_ -> mk_id name) params in
let args,sort = NCicReduction.split_prods ~subst:[] [] (-1) ty in
let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
let params = List.rev_map (function name,_ -> mk_id name) params in
let args,sort = NCicReduction.split_prods ~subst:[] [] (-1) ty in