let pp fmt s =
  if not(is_empty s) then
    begin
      if !Fact.print_justification then
        Pretty.set Fact.Equal.pp fmt (to_equalities s)
      else 
        Pretty.map Term.pp (Pretty.set Term.pp) fmt (to_list s);
      if not(s.cnstrnt == Term.Var.Map.empty) then
        begin
          Pretty.string fmt "\nwith:";
          let l = Term.Var.Map.fold (fun x (c, _) acc -> (x, c) :: acc) s.cnstrnt [] in
            Pretty.map Term.pp Var.Cnstrnt.pp fmt l
        end 
    end