let term_mk_add = Arith.mk_add