let rec map f a =
  match a with
    | Term.App((Sym.Arith(op), _), al, _) ->
        (match op, al with
           | Sym.Num _, [] -> 
               a
           | Sym.Multq(q), [x] ->
               let x' = map f x in
                 if x == x' then a else 
                   mk_multq q x'
           | Sym.Add, [x; y] -> 
               let x' = map f x and y' = map f y in
                 if x == x' && y == y' then a else 
                   mk_add x' y'
           | Sym.Add, xl -> 
               let xl' = Term.mapl (map f) xl in
                 if xl == xl' then a else
                   mk_addl xl'
           | _ -> 
               assert false)
    | _ ->
        f a