let arity_l = cut_last (list_of_prod arity) in
let rightparam_tys = cut_first nleft arity_l in
let theorem = build_theorem rightparam_tys arity_l arity cons_list
let arity_l = cut_last (list_of_prod arity) in
let rightparam_tys = cut_first nleft arity_l in
let theorem = build_theorem rightparam_tys arity_l arity cons_list