let pp fmt (a, rho) =
  pp_justification fmt rho;
  Atom.pp fmt a