let pp fmt (atm, _) =
  match atm with 
    | TT -> Pretty.string fmt "tt"
    | FF -> Pretty.string fmt "ff"
    | Equal(a, b) -> Pretty.infix Term.pp "=" Term.pp fmt (a, b)
    | Diseq(a, b) -> Pretty.infix Term.pp "<>" Term.pp fmt (a, b)
    | Nonneg(a) -> Pretty.post Term.pp fmt (a, ">=0")
    | Pos(a) -> Pretty.post Term.pp fmt (a, ">0")