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