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