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