let rec pp fmt = function
  | True -> 
      Pretty.string fmt "tt"
  | False -> 
      Pretty.string fmt "ff"
  | Var(x) -> 
      Name.pp fmt x
  | Atom(a) -> 
      Atom.pp fmt a
  | Disj(pl) -> 
      Pretty.infixl pp " | " fmt pl
  | Iff(p, q) -> 
      Pretty.infix pp " <=> " pp fmt (p, q)
  | Neg(p) -> 
      Pretty.string fmt "~("; pp fmt p; Pretty.string fmt ")"
  | Let(x, p, q) ->
      Pretty.mixfix "let" Name.pp ":=" pp "in" pp "end" fmt (x, p, q)
  | Ite(p, q, r) ->
      Pretty.mixfix "if" pp "then" pp "else" pp "end" fmt (p, q, r)