let constant_of = function
  | Term.App((Sym.Arith(op), _), l, _) ->
      (match op, l with
         | Sym.Num(q), [] -> q
         | Sym.Add, (Term.App((Sym.Arith(Sym.Num(q)), _), [], _) :: _) -> q
         | _ -> Q.zero)
    | _ ->
        Q.zero