sig
  type seq_t
  type proof_t
  type axiom_f = Sigs.PROOFRULE.seq_t -> string option
  type infrule_app =
      (Sigs.PROOFRULE.seq_t * Tagpairs.t * Tagpairs.t) list * string
  type infrule_f = Sigs.PROOFRULE.seq_t -> Sigs.PROOFRULE.infrule_app list
  type backrule_f =
      Sigs.PROOFRULE.seq_t ->
      Sigs.PROOFRULE.seq_t -> (Tagpairs.t * string) list
  type select_f = int -> Sigs.PROOFRULE.proof_t -> int list
  type t =
      int ->
      Sigs.PROOFRULE.proof_t -> (int list * Sigs.PROOFRULE.proof_t) Blist.t
  val mk_axiom : Sigs.PROOFRULE.axiom_f -> Sigs.PROOFRULE.t
  val mk_infrule : Sigs.PROOFRULE.infrule_f -> Sigs.PROOFRULE.t
  val mk_backrule :
    bool ->
    Sigs.PROOFRULE.select_f -> Sigs.PROOFRULE.backrule_f -> Sigs.PROOFRULE.t
  val all_nodes : Sigs.PROOFRULE.select_f
  val closed_nodes : Sigs.PROOFRULE.select_f
  val ancestor_nodes : Sigs.PROOFRULE.select_f
  val syntactically_equal_nodes : Sigs.PROOFRULE.select_f
  val fail : Sigs.PROOFRULE.t
  val identity : Sigs.PROOFRULE.t
  val attempt : Sigs.PROOFRULE.t -> Sigs.PROOFRULE.t
  val compose : Sigs.PROOFRULE.t -> Sigs.PROOFRULE.t -> Sigs.PROOFRULE.t
  val compose_pairwise :
    Sigs.PROOFRULE.t -> Sigs.PROOFRULE.t list -> Sigs.PROOFRULE.t
  val choice : Sigs.PROOFRULE.t list -> Sigs.PROOFRULE.t
  val first : Sigs.PROOFRULE.t list -> Sigs.PROOFRULE.t
  val sequence : Sigs.PROOFRULE.t list -> Sigs.PROOFRULE.t
  val conditional :
    (Sigs.PROOFRULE.seq_t -> bool) -> Sigs.PROOFRULE.t -> Sigs.PROOFRULE.t
  val combine_axioms :
    Sigs.PROOFRULE.t -> Sigs.PROOFRULE.t -> Sigs.PROOFRULE.t
end