sig
  type t = Proof.parent
  val from : Proof.proof -> Proof.Parent.t
  val from_subst :
    Proof.proof Logtk.Scoped.t -> Logtk.Subst.t -> Proof.Parent.t
  val add_subst :
    Proof.Parent.t Logtk.Scoped.t -> Logtk.Subst.t -> Proof.Parent.t
  val proof : Proof.Parent.t -> Proof.proof
  val subst : Proof.Parent.t -> Logtk.Subst.t list
end