let rec term_mk_multl = function
  | [] -> Arith.mk_one
  | [a] -> a
  | a :: b :: l -> term_mk_multl (term_mk_mult a b :: l)