sig
  type abstract_node
  val mk_abs_node :
    Tags.t ->
    (int * Tagpairs.t * Tagpairs.t) list -> Soundcheck.abstract_node
  type t = Soundcheck.abstract_node Int.Map.t
  val build_proof :
    (int * int list * (int * (int * int) list * (int * int) list) list) list ->
    Soundcheck.t
  val check_proof : Soundcheck.t -> bool
  val pp : Format.formatter -> Soundcheck.t -> unit
end