let rec map f a =
  match a with
    | App(Arith(op), l) ->
        (match op, l with
           | Num _, [] -> 
               a
           | Multq(q), [x] ->
               let x' = map f x in
                 if x == x' then a else 
                   mk_multq q x'
           | 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'
           | Add, xl -> 
               let xl' = Term.mapl (map f) xl in
                 if xl == xl' then a else
                   mk_addl xl'
           | _ -> 
               assert false)
    | _ ->
        f a