let pp fmt j =
  match !proofmode with
    | No -> Pretty.string fmt "Unjustified"
    | Dep -> 
        let al = Atom.Set.elements j in
          Pretty.set Atom.pp fmt al