let nonconstant_of a =
  match a with
    | Term.App((Sym.Arith(op), _), l, _) ->
        (match op, l with
           | Sym.Num(_), [] -> 
               mk_zero()
           | Sym.Add, (Term.App((Sym.Arith(Sym.Num(_)), _), [], _) :: al) ->
               Term.App.mk_app Sym.Arith.mk_add al
           | _ -> 
               a)
    | _ ->
        a