sig
  type t = ProverWhy3.goal
  val compare : ProverWhy3.Goal.t -> ProverWhy3.Goal.t -> int
  val pretty : Stdlib.Format.formatter -> ProverWhy3.Goal.t -> unit
end