sig
  type goal = { file : string; theory : string; goal : string; }
  val assemble_goal : Wpo.t -> (string list * ProverWhy3.goal) option
  val prove : ?timeout:int -> prover:string -> Wpo.t -> VCS.result Task.task
  module Goal :
    sig
      type t = ProverWhy3.goal
      val compare : ProverWhy3.Goal.t -> ProverWhy3.Goal.t -> int
      val pretty : Stdlib.Format.formatter -> ProverWhy3.Goal.t -> unit
    end
end