module VC_Check: sig .. end
sig
end
type t = {
qed : Wp.Lang.F.term;
Wp.Lang.F.term
raw : Wp.Lang.F.term;
goal : Wp.Lang.F.pred;
Wp.Lang.F.pred