Module Wpo.VC_Check

module VC_Check: sig .. end

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