sig
  type t = { qed : Lang.F.term; raw : Lang.F.term; goal : Lang.F.pred; }
  val pretty : Format.formatter -> Wpo.VC_Check.t -> unit
end