Module Wp.Wpo.VC_Check

module VC_Check: sig .. end

type t = {
   qed : Wp.Lang.F.term;
   raw : Wp.Lang.F.term;
   goal : Wp.Lang.F.pred;
}